--- a/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
(**** 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*)
@@ -36,7 +36,7 @@
| "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