src/HOL/Induct/Com.thy
changeset 41818 6d4c3ee8219d
parent 36862 952b2b102a0a
child 44174 d1d79f0e1ea6
     1.1 --- a/src/HOL/Induct/Com.thy	Tue Feb 22 16:47:18 2011 +0100
     1.2 +++ b/src/HOL/Induct/Com.thy	Tue Feb 22 17:06:14 2011 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  theory Com imports Main begin
     1.5  
     1.6  typedecl loc
     1.7 -types  state = "loc => nat"
     1.8 +type_synonym state = "loc => nat"
     1.9  
    1.10  datatype
    1.11    exp = N nat