# HG changeset patch
# User hoelzl
# Date 1246352342 -7200
# Node ID 90ec13cf7ab0a6f858baff71a3985b78e66e1c70
# Parent  e391eee8bf146e213e036c3e501d8b60a44e29c3
removed latex markup - there is no document generated from Decision_Procs/ex

diff -r e391eee8bf14 -r 90ec13cf7ab0 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Mon Jun 29 23:29:11 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Tue Jun 30 10:59:02 2009 +0200
@@ -10,7 +10,7 @@
 
 The approximation method has the following syntax:
 
-\verb| approximate "prec" (splitting: "x" = "depth" and "y" = "depth" \<dots>)? (taylor: "z" = "derivates")? |
+approximate "prec" (splitting: "x" = "depth" and "y" = "depth" ...)? (taylor: "z" = "derivates")?
 
 Here "prec" specifies the precision used in all computations, it is specified as
 number of bits to calculate. In the proposition to prove an arbitrary amount of
@@ -24,8 +24,8 @@
 
 To use interval splitting add for each variable whos interval should be splitted
 to the "splitting:" parameter. The parameter specifies how often each interval
-should be divided, e.g. when x = 16 is specified, there will be $65536 = 2^16$ intervals
-to be calculated.
+should be divided, e.g. when x = 16 is specified, there will be @{term "65536 = 2^16"}
+intervals to be calculated.
 
 To use taylor series expansion specify the variable to derive. You need to
 specify the amount of derivations to compute. When using taylor series expansion