src/HOL/Induct/Com.thy
changeset 58305 57752a91eec4
parent 44965 9e17d632a9ed
child 58310 91ea607a34d8
     1.1 --- a/src/HOL/Induct/Com.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  typedecl loc
     1.5  type_synonym state = "loc => nat"
     1.6  
     1.7 -datatype
     1.8 +datatype_new
     1.9    exp = N nat
    1.10        | X loc
    1.11        | Op "nat => nat => nat" exp exp