use antiquotations instead of raw TeX code;
authorwenzelm
Sun Jun 03 23:16:46 2007 +0200 (2007-06-03)
changeset 2321801c4d19f597e
parent 23217 8eac3bda1063
child 23219 87ad6e8a5f2c
use antiquotations instead of raw TeX code;
tuned document;
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/src/HOL/ex/Arith_Examples.thy	Sun Jun 03 23:16:45 2007 +0200
     1.2 +++ b/src/HOL/ex/Arith_Examples.thy	Sun Jun 03 23:16:46 2007 +0200
     1.3 @@ -3,35 +3,35 @@
     1.4      Author: Tjark Weber
     1.5  *)
     1.6  
     1.7 -header {* {\tt arith} *}
     1.8 +header {* Arithmetic *}
     1.9  
    1.10  theory Arith_Examples imports Main begin
    1.11  
    1.12  text {*
    1.13 -  The {\tt arith} tactic is used frequently throughout the Isabelle
    1.14 +  The @{text arith} method is used frequently throughout the Isabelle
    1.15    distribution.  This file merely contains some additional tests and special
    1.16    corner cases.  Some rather technical remarks:
    1.17  
    1.18 -  \verb!fast_arith_tac! is a very basic version of the tactic.  It performs no
    1.19 +  @{ML fast_arith_tac} is a very basic version of the tactic.  It performs no
    1.20    meta-to-object-logic conversion, and only some splitting of operators.
    1.21 -  \verb!simple_arith_tac! performs meta-to-object-logic conversion, full
    1.22 -  splitting of operators, and NNF normalization of the goal.  The {\tt arith}
    1.23 -  tactic combines them both, and tries other tactics (e.g.~{\tt presburger})
    1.24 +  @{ML simple_arith_tac} performs meta-to-object-logic conversion, full
    1.25 +  splitting of operators, and NNF normalization of the goal.  The @{text arith}
    1.26 +  method combines them both, and tries other methods (e.g.~@{text presburger})
    1.27    as well.  This is the one that you should use in your proofs!
    1.28  
    1.29 -  An {\tt arith}-based simproc is available as well
    1.30 -  (see \verb!Fast_Arith.lin_arith_prover!),
    1.31 +  An @{text arith}-based simproc is available as well
    1.32 +  (see @{ML Fast_Arith.lin_arith_prover}),
    1.33    which---for performance reasons---however
    1.34 -  does even less splitting than \verb!fast_arith_tac! at the moment (namely
    1.35 +  does even less splitting than @{ML fast_arith_tac} at the moment (namely
    1.36    inequalities only).  (On the other hand, it does take apart conjunctions,
    1.37 -  which \verb!fast_arith_tac! currently does not do.)
    1.38 +  which @{ML fast_arith_tac} currently does not do.)
    1.39  *}
    1.40  
    1.41  (*
    1.42  ML {* set trace_arith; *}
    1.43  *)
    1.44  
    1.45 -section {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    1.46 +subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    1.47             @{term HOL.minus}, @{term nat}, @{term Divides.mod},
    1.48             @{term Divides.div} *}
    1.49  
    1.50 @@ -130,7 +130,8 @@
    1.51    apply (tactic {* LA_Data_Ref.pre_tac 1 *})
    1.52  oops
    1.53  
    1.54 -section {* Meta-Logic *}
    1.55 +
    1.56 +subsection {* Meta-Logic *}
    1.57  
    1.58  lemma "x < Suc y == x <= y"
    1.59    by (tactic {* simple_arith_tac 1 *})
    1.60 @@ -138,7 +139,8 @@
    1.61  lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
    1.62    by (tactic {* simple_arith_tac 1 *})
    1.63  
    1.64 -section {* Various Other Examples *}
    1.65 +
    1.66 +subsection {* Various Other Examples *}
    1.67  
    1.68  lemma "(x < Suc y) = (x <= y)"
    1.69    by (tactic {* simple_arith_tac 1 *})