equal
deleted
inserted
replaced
2003 in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
2003 in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
2004 end; |
2004 end; |
2005 *} |
2005 *} |
2006 |
2006 |
2007 use "cooper_tac.ML" |
2007 use "cooper_tac.ML" |
2008 setup "Cooper_Tac.setup" |
2008 |
|
2009 method_setup cooper = {* |
|
2010 Args.mode "no_quantify" >> |
|
2011 (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q))) |
|
2012 *} "decision procedure for linear integer arithmetic" |
|
2013 |
2009 |
2014 |
2010 text {* Tests *} |
2015 text {* Tests *} |
2011 |
2016 |
2012 lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)" |
2017 lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)" |
2013 by cooper |
2018 by cooper |