src/HOL/Decision_Procs/Ferrack.thy

 
   (*********************************************************************************)
   (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
   (*********************************************************************************)
 
-datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
+datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
   | Mul int num 
 
   (* A size for num to make inductive proofs simpler*)
 primrec num_size :: "num \<Rightarrow> nat" where
   "num_size (C c) = 1"

 | "Inum bs (Neg a) = -(Inum bs a)"
 | "Inum bs (Add a b) = Inum bs a + Inum bs b"
 | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
 | "Inum bs (Mul c a) = (real c) * Inum bs a"
     (* FORMULAE *)
-datatype fm  = 
+datatype_new fm  = 
   T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
 
 
   (* A size for fm *)