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