# HG changeset patch
# User nipkow
# Date 1180878275 -7200
# Node ID 4d56ad10b5e851e5c94cb1c03f234cf88cd23e5a
# Parent  a0cb15114e7a376f7bd0035255e3c94d3917deb8
fixed tex error

diff -r a0cb15114e7a -r 4d56ad10b5e8 src/HOL/ex/Arith_Examples.thy
--- 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.)
 *}
 
 (*