equal
deleted
inserted
replaced
2002 in (Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
2002 in (Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
2003 end; |
2003 end; |
2004 *} |
2004 *} |
2005 |
2005 |
2006 use "ferrack_tac.ML" |
2006 use "ferrack_tac.ML" |
2007 setup Ferrack_Tac.setup |
2007 |
|
2008 method_setup rferrack = {* |
|
2009 Args.mode "no_quantify" >> |
|
2010 (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q))) |
|
2011 *} "decision procedure for linear real arithmetic" |
|
2012 |
2008 |
2013 |
2009 lemma |
2014 lemma |
2010 fixes x :: real |
2015 fixes x :: real |
2011 shows "2 * x \<le> 2 * x \<and> 2 * x \<le> 2 * x + 1" |
2016 shows "2 * x \<le> 2 * x \<and> 2 * x \<le> 2 * x + 1" |
2012 apply rferrack |
2017 apply rferrack |