equal
deleted
inserted
replaced
2001 |
2001 |
2002 text \<open> |
2002 text \<open> |
2003 \begin{matharray}{rcl} |
2003 \begin{matharray}{rcl} |
2004 @{method_def (HOL) arith} & : & \<open>method\<close> \\ |
2004 @{method_def (HOL) arith} & : & \<open>method\<close> \\ |
2005 @{attribute_def (HOL) arith} & : & \<open>attribute\<close> \\ |
2005 @{attribute_def (HOL) arith} & : & \<open>attribute\<close> \\ |
2006 @{attribute_def (HOL) arith_split} & : & \<open>attribute\<close> \\ |
2006 @{attribute_def (HOL) linarith_split} & : & \<open>attribute\<close> \\ |
2007 \end{matharray} |
2007 \end{matharray} |
2008 |
2008 |
2009 \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \<open>nat\<close>, |
2009 \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \<open>nat\<close>, |
2010 \<open>int\<close>, \<open>real\<close>). Any current facts are inserted into the goal before running |
2010 \<open>int\<close>, \<open>real\<close>). Any current facts are inserted into the goal before running |
2011 the procedure. |
2011 the procedure. |
2012 |
2012 |
2013 \<^descr> @{attribute (HOL) arith} declares facts that are supplied to the |
2013 \<^descr> @{attribute (HOL) arith} declares facts that are supplied to the |
2014 arithmetic provers implicitly. |
2014 arithmetic provers implicitly. |
2015 |
2015 |
2016 \<^descr> @{attribute (HOL) arith_split} attribute declares case split rules to be |
2016 \<^descr> @{attribute (HOL) linarith_split} attribute declares case split rules to be |
2017 expanded before @{method (HOL) arith} is invoked. |
2017 expanded before @{method (HOL) arith} is invoked. |
2018 |
2018 |
2019 |
2019 |
2020 Note that a simpler (but faster) arithmetic prover is already invoked by the |
2020 Note that a simpler (but faster) arithmetic prover is already invoked by the |
2021 Simplifier. |
2021 Simplifier. |