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. *}
```