changeset 63167 | 0909deb8059b |
parent 58310 | 91ea607a34d8 |
child 66453 | cc19f7ca2ed6 |
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Thu May 26 17:51:22 2016 +0200 @@ -2,11 +2,11 @@ imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck" begin -subsection {* IMP *} +subsection \<open>IMP\<close> -text {* +text \<open> In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While. -*} +\<close> type_synonym var = unit type_synonym state = bool