src/HOL/Predicate_Compile_Examples/IMP_3.thy
changeset 42031 2de57cda5b24
parent 41413 64cd30d6b0b8
child 43686 bc7d63c7fd6f
     1.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -8,9 +8,8 @@
     1.4    In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While.
     1.5  *}
     1.6  
     1.7 -types
     1.8 -  var = unit
     1.9 -  state = int
    1.10 +type_synonym var = unit
    1.11 +type_synonym state = int
    1.12  
    1.13  datatype com =
    1.14    Skip |