diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_2.thy --- 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 |