# HG changeset patch
# User haftmann
# Date 1273660311 -7200
# Node ID b897bd9ca71bfb1cb58069105e9c312b968bd2ac
# Parent  691a55e1aeb2695cf0a3357a2cc14d0a5172d824
tuned test problems

diff -r 691a55e1aeb2 -r b897bd9ca71b src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Wed May 12 12:20:16 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed May 12 12:31:51 2010 +0200
@@ -5771,25 +5771,25 @@
   using qelim_ci[OF mirlfr] prep by (auto simp add: mirlfrqe_def)
 
 definition
-  "test1 (u\<Colon>unit) = mircfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
+  "problem1 = A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0))))))"
 
 definition
-  "test2 (u\<Colon>unit) = mircfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
+  "problem2 = A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0))))"
 
 definition
-  "test3 (u\<Colon>unit) = mirlfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
+  "problem3 = A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0))))))"
 
 definition
-  "test4 (u\<Colon>unit) = mirlfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
-
-definition
-  "test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
-
-ML {* @{code test1} () *}
-ML {* @{code test2} () *}
-ML {* @{code test3} () *}
-ML {* @{code test4} () *}
-ML {* @{code test5} () *}
+  "problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))"
+
+ML {* @{code mircfrqe} @{code problem1} *}
+ML {* @{code mirlfrqe} @{code problem1} *}  
+ML {* @{code mircfrqe} @{code problem2} *}
+ML {* @{code mirlfrqe} @{code problem2} *}  
+ML {* @{code mircfrqe} @{code problem3} *}
+ML {* @{code mirlfrqe} @{code problem3} *}  
+ML {* @{code mircfrqe} @{code problem4} *}
+ML {* @{code mirlfrqe} @{code problem4} *}
 
 (*code_reflect Mir
   functions mircfrqe mirlfrqe