Email Gateway (Aug 18 2022 at 13:17): Email Gateway (Aug 18 2022 at 13:17):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi,
in HOL/Library/State_Monad.thy, HOL/ex/Random.thy is mentioned as an
example for the
do ... done - syntax.
However, it seems as if this theory has been removed in the
2009-version. (The reference in State_Monad.thy is still there).
Email Gateway (Aug 18 2022 at 13:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
these theory references are not formally checked; the Random theory now
resides in HOL/Library.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 13:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
...even more, Random.thy does not use State_Monad.thy any longer.
But there is an example in HOL/Extraction/Higman.thy
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 08:18 UTC