src/HOL/Predicate_Compile_Examples/IMP_1.thy
changeset 42031 2de57cda5b24
parent 41413 64cd30d6b0b8
child 42397 13798dcbdca5
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.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, and IF.
 *}
 
-types
-  var = unit
-  state = bool
+type_synonym var = unit
+type_synonym state = bool
 
 datatype com =
   Skip |