
diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Reflection_Examples.thy
--- a/src/HOL/ex/Reflection_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Reflection_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -46,7 +46,7 @@
 text {* Example 1 : Propositional formulae and NNF. *}
 text {* The type @{text fm} represents simple propositional formulae: *}
 
-datatype form = TrueF | FalseF | Less nat nat
+datatype_new form = TrueF | FalseF | Less nat nat
   | And form form | Or form form | Neg form | ExQ form
 
 primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
@@ -66,7 +66,7 @@
   apply reify
   oops
 
-datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
+datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
 
 primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
 where
@@ -135,7 +135,7 @@
 text {* Example 2: Simple arithmetic formulae *}
 
 text {* The type @{text num} reflects linear expressions over natural number *}
-datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
+datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
 
 text {* This is just technical to make recursive definitions easier. *}
 primrec num_size :: "num \<Rightarrow> nat" 
@@ -252,7 +252,7 @@
 
 text {* Let's lift this to formulae and see what happens *}
 
-datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
+datatype_new aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   Conj aform aform | Disj aform aform | NEG aform | T | F
 
 primrec linaformsize:: "aform \<Rightarrow> nat"
@@ -331,7 +331,7 @@
   one envornement of different types and show that automatic reification also deals with
   bindings *}
   
-datatype rb = BC bool | BAnd rb rb | BOr rb rb
+datatype_new rb = BC bool | BAnd rb rb | BOr rb rb
 
 primrec Irb :: "rb \<Rightarrow> bool"
 where
@@ -343,7 +343,7 @@
   apply (reify Irb.simps)
 oops
 
-datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
+datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
   | INeg rint | ISub rint rint
 
 primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
@@ -370,7 +370,7 @@
   apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
   oops
 
-datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
+datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
 
 primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
 where
@@ -387,7 +387,7 @@
   apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
   oops
 
-datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
+datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
   | NNeg rnat | NSub rnat rnat | Nlgth rlist
 
 primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
@@ -418,7 +418,7 @@
      ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
   oops
 
-datatype rifm = RT | RF | RVar nat
+datatype_new rifm = RT | RF | RVar nat
   | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
   | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
   | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
@@ -451,7 +451,7 @@
 
 text {* An example for equations containing type variables *}
 
-datatype prod = Zero | One | Var nat | Mul prod prod 
+datatype_new prod = Zero | One | Var nat | Mul prod prod 
   | Pw prod nat | PNM nat nat prod
 
 primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
@@ -463,7 +463,7 @@
 | "Iprod (Pw a n) vs = Iprod a vs ^ n"
 | "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
 
-datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
+datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   | Or sgn sgn | And sgn sgn
 
 primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"




