changeset 42031 | 2de57cda5b24 |
parent 41413 | 64cd30d6b0b8 |
child 42397 | 13798dcbdca5 |
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Mar 18 18:19:42 2011 +0100 @@ -8,9 +8,8 @@ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While. *} -types - var = unit - state = bool +type_synonym var = unit +type_synonym state = bool datatype com = Skip |