# HG changeset patch # User wenzelm # Date 1415223434 -3600 # Node ID f323497583d108b27f6764446e5924cf359afe9b # Parent 58bedbc189155aaaba97e37a50b0bd72de3c7b84 more symbols; diff -r 58bedbc18915 -r f323497583d1 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Wed Nov 05 22:17:05 2014 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Wed Nov 05 22:37:14 2014 +0100 @@ -5667,19 +5667,19 @@ *} "decision procedure for MIR arithmetic" -lemma "ALL (x::real). (\x\ = \x\ = (x = real \x\))" +lemma "\x::real. (\x\ = \x\ = (x = real \x\))" by mir -lemma "ALL (x::real). real (2::int)*x - (real (1::int)) < real \x\ + real \x\ \ real \x\ + real \x\ \ real (2::int)*x + (real (1::int))" +lemma "\x::real. real (2::int)*x - (real (1::int)) < real \x\ + real \x\ \ real \x\ + real \x\ \ real (2::int)*x + (real (1::int))" by mir -lemma "ALL (x::real). 2*\x\ \ \2*x\ \ \2*x\ \ 2*\x+1\" +lemma "\x::real. 2*\x\ \ \2*x\ \ \2*x\ \ 2*\x+1\" by mir -lemma "ALL (x::real). \y \ x. (\x\ = \y\)" +lemma "\x::real. \y \ x. (\x\ = \y\)" by mir -lemma "ALL (x::real) (y::real). \x\ = \y\ \ 0 \ abs (y - x) \ abs (y - x) \ 1" +lemma "\(x::real) (y::real). \x\ = \y\ \ 0 \ abs (y - x) \ abs (y - x) \ 1" by mir end