src/HOL/IMP/Types.thy

 text {* We build on @{theory Complex_Main} instead of @{theory Main} to access
 the real numbers. *}
 
 subsection "Arithmetic Expressions"
 
-datatype_new val = Iv int | Rv real
+datatype val = Iv int | Rv real
 
 type_synonym vname = string
 type_synonym state = "vname \<Rightarrow> val"
 
 text_raw{*\snip{aexptDef}{0}{2}{% *}
-datatype_new aexp =  Ic int | Rc real | V vname | Plus aexp aexp
+datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
 text_raw{*}%endsnip*}
 
 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
 "taval (Ic i) s (Iv i)" |
 "taval (Rc r) s (Rv r)" |

   "taval (V x) s v"
   "taval (Plus a1 a2) s v"
 
 subsection "Boolean Expressions"
 
-datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
 inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
 "tbval (Bc v) s v" |
 "tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
 "tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |

 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
 
 subsection "Syntax of Commands"
 (* a copy of Com.thy - keep in sync! *)
 
-datatype_new
+datatype
   com = SKIP 
       | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
       | Seq    com  com         ("_;; _"  [60, 61] 60)
       | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
       | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)

 
 lemmas small_step_induct = small_step.induct[split_format(complete)]
 
 subsection "The Type System"
 
-datatype_new ty = Ity | Rty
+datatype ty = Ity | Rty
 
 type_synonym tyenv = "vname \<Rightarrow> ty"
 
 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)