removed latex markup - there is no document generated from Decision_Procs/ex
authorhoelzl
Tue, 30 Jun 2009 10:59:02 +0200
changeset 31864 90ec13cf7ab0
parent 31863 e391eee8bf14
child 31865 5e97c4abd18e
removed latex markup - there is no document generated from Decision_Procs/ex
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