--- a/src/HOL/Decision_Procs/MIR.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Tue Sep 09 20:51:36 2014 +0200
@@ -105,7 +105,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 | Floor num| CF int num num
(* A size for num to make inductive proofs simpler*)
@@ -188,7 +188,7 @@
(* FORMULAE *)
-datatype fm =
+datatype_new fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm