fixed tex error
authornipkow
Sun Jun 03 15:44:35 2007 +0200 (2007-06-03)
changeset 232114d56ad10b5e8
parent 23210 a0cb15114e7a
child 23212 82881b1ae9c6
fixed tex error
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/src/HOL/ex/Arith_Examples.thy	Sun Jun 03 13:19:03 2007 +0200
     1.2 +++ b/src/HOL/ex/Arith_Examples.thy	Sun Jun 03 15:44:35 2007 +0200
     1.3 @@ -12,18 +12,19 @@
     1.4    distribution.  This file merely contains some additional tests and special
     1.5    corner cases.  Some rather technical remarks:
     1.6  
     1.7 -  {\tt fast_arith_tac} is a very basic version of the tactic.  It performs no
     1.8 +  \verb!fast_arith_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 -  {\tt simple_arith_tac} performs meta-to-object-logic conversion, full
    1.11 +  \verb!simple_arith_tac! performs meta-to-object-logic conversion, full
    1.12    splitting of operators, and NNF normalization of the goal.  The {\tt arith}
    1.13    tactic combines them both, and tries other tactics (e.g.~{\tt presburger})
    1.14    as well.  This is the one that you should use in your proofs!
    1.15  
    1.16 -  An {\tt arith}-based simproc is available as well (see {\tt
    1.17 -  Fast_Arith.lin_arith_prover}), which---for performance reasons---however
    1.18 -  does even less splitting than {\tt fast_arith_tac} at the moment (namely
    1.19 +  An {\tt arith}-based simproc is available as well
    1.20 +  (see \verb!Fast_Arith.lin_arith_prover!),
    1.21 +  which---for performance reasons---however
    1.22 +  does even less splitting than \verb!fast_arith_tac! at the moment (namely
    1.23    inequalities only).  (On the other hand, it does take apart conjunctions,
    1.24 -  which {\tt fast_arith_tac} currently does not do.)
    1.25 +  which \verb!fast_arith_tac! currently does not do.)
    1.26  *}
    1.27  
    1.28  (*