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