1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed May 12 12:20:16 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed May 12 12:31:51 2010 +0200
     1.3 @@ -5771,25 +5771,25 @@
     1.4    using qelim_ci[OF mirlfr] prep by (auto simp add: mirlfrqe_def)
     1.5  
     1.6  definition
     1.7 -  "test1 (u\<Colon>unit) = mircfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
     1.8 +  "problem1 = A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0))))))"
     1.9  
    1.10  definition
    1.11 -  "test2 (u\<Colon>unit) = mircfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
    1.12 +  "problem2 = A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0))))"
    1.13  
    1.14  definition
    1.15 -  "test3 (u\<Colon>unit) = mirlfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
    1.16 +  "problem3 = A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0))))))"
    1.17  
    1.18  definition
    1.19 -  "test4 (u\<Colon>unit) = mirlfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
    1.20 -
    1.21 -definition
    1.22 -  "test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
    1.23 -
    1.24 -ML {* @{code test1} () *}
    1.25 -ML {* @{code test2} () *}
    1.26 -ML {* @{code test3} () *}
    1.27 -ML {* @{code test4} () *}
    1.28 -ML {* @{code test5} () *}
    1.29 +  "problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))"
    1.30 +
    1.31 +ML {* @{code mircfrqe} @{code problem1} *}
    1.32 +ML {* @{code mirlfrqe} @{code problem1} *}  
    1.33 +ML {* @{code mircfrqe} @{code problem2} *}
    1.34 +ML {* @{code mirlfrqe} @{code problem2} *}  
    1.35 +ML {* @{code mircfrqe} @{code problem3} *}
    1.36 +ML {* @{code mirlfrqe} @{code problem3} *}  
    1.37 +ML {* @{code mircfrqe} @{code problem4} *}
    1.38 +ML {* @{code mirlfrqe} @{code problem4} *}
    1.39  
    1.40  (*code_reflect Mir
    1.41    functions mircfrqe mirlfrqe