summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/Arith_Examples.thy

changeset 31101 | 26c7bb764a38 |

parent 31100 | 6a2e67fe4488 |

child 34974 | 18b41bba42b5 |

1.1 --- a/src/HOL/ex/Arith_Examples.thy Mon May 11 15:18:32 2009 +0200 1.2 +++ b/src/HOL/ex/Arith_Examples.thy Mon May 11 15:57:29 2009 +0200 1.3 @@ -13,18 +13,18 @@ 1.4 distribution. This file merely contains some additional tests and special 1.5 corner cases. Some rather technical remarks: 1.6 1.7 - @{ML fast_arith_tac} is a very basic version of the tactic. It performs no 1.8 + @{ML Lin_Arith.simple_tac} is a very basic version of the tactic. It performs no 1.9 meta-to-object-logic conversion, and only some splitting of operators. 1.10 - @{ML linear_arith_tac} performs meta-to-object-logic conversion, full 1.11 + @{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full 1.12 splitting of operators, and NNF normalization of the goal. The @{text arith} 1.13 method combines them both, and tries other methods (e.g.~@{text presburger}) 1.14 as well. This is the one that you should use in your proofs! 1.15 1.16 An @{text arith}-based simproc is available as well (see @{ML 1.17 - Lin_Arith.lin_arith_simproc}), which---for performance 1.18 - reasons---however does even less splitting than @{ML fast_arith_tac} 1.19 + Lin_Arith.simproc}), which---for performance 1.20 + reasons---however does even less splitting than @{ML Lin_Arith.simple_tac} 1.21 at the moment (namely inequalities only). (On the other hand, it 1.22 - does take apart conjunctions, which @{ML fast_arith_tac} currently 1.23 + does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently 1.24 does not do.) 1.25 *} 1.26 1.27 @@ -208,13 +208,13 @@ 1.28 (* preprocessing negates the goal and tries to compute its negation *) 1.29 (* normal form, which creates lots of separate cases for this *) 1.30 (* disjunction of conjunctions *) 1.31 -(* by (tactic {* linear_arith_tac 1 *}) *) 1.32 +(* by (tactic {* Lin_Arith.tac 1 *}) *) 1.33 oops 1.34 1.35 lemma "2 * (x::nat) ~= 1" 1.36 (* FIXME: this is beyond the scope of the decision procedure at the moment, *) 1.37 (* because its negation is satisfiable in the rationals? *) 1.38 -(* by (tactic {* fast_arith_tac 1 *}) *) 1.39 +(* by (tactic {* Lin_Arith.simple_tac 1 *}) *) 1.40 oops 1.41 1.42 text {* Constants. *}