src/HOL/Decision_Procs/Ferrack.thy

--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -2004,7 +2004,12 @@
 *}
 
 use "ferrack_tac.ML"
-setup Ferrack_Tac.setup
+
+method_setup rferrack = {*
+  Args.mode "no_quantify" >>
+    (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
+*} "decision procedure for linear real arithmetic"
+
 
 lemma
   fixes x :: real