--- a/src/HOL/ex/Arith_Examples.thy Sun Jun 03 13:19:03 2007 +0200
+++ b/src/HOL/ex/Arith_Examples.thy Sun Jun 03 15:44:35 2007 +0200
@@ -12,18 +12,19 @@
distribution. This file merely contains some additional tests and special
corner cases. Some rather technical remarks:
- {\tt fast_arith_tac} is a very basic version of the tactic. It performs no
+ \verb!fast_arith_tac! is a very basic version of the tactic. It performs no
meta-to-object-logic conversion, and only some splitting of operators.
- {\tt simple_arith_tac} performs meta-to-object-logic conversion, full
+ \verb!simple_arith_tac! performs meta-to-object-logic conversion, full
splitting of operators, and NNF normalization of the goal. The {\tt arith}
tactic combines them both, and tries other tactics (e.g.~{\tt presburger})
as well. This is the one that you should use in your proofs!
- An {\tt arith}-based simproc is available as well (see {\tt
- Fast_Arith.lin_arith_prover}), which---for performance reasons---however
- does even less splitting than {\tt fast_arith_tac} at the moment (namely
+ An {\tt arith}-based simproc is available as well
+ (see \verb!Fast_Arith.lin_arith_prover!),
+ which---for performance reasons---however
+ does even less splitting than \verb!fast_arith_tac! at the moment (namely
inequalities only). (On the other hand, it does take apart conjunctions,
- which {\tt fast_arith_tac} currently does not do.)
+ which \verb!fast_arith_tac! currently does not do.)
*}
(*