src/HOL/Decision_Procs/MIR.thy
changeset 47432 e1576d13e933
parent 47142 d64fa2ca54b8
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -5635,7 +5635,12 @@
     1.4  *}
     1.5  
     1.6  use "mir_tac.ML"
     1.7 -setup "Mir_Tac.setup"
     1.8 +
     1.9 +method_setup mir = {*
    1.10 +  Args.mode "no_quantify" >>
    1.11 +    (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
    1.12 +*} "decision procedure for MIR arithmetic"
    1.13 +
    1.14  
    1.15  lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
    1.16    by mir