NEWS
changeset 30439 57c68b3af2ea
parent 30415 9501af91c4a3
child 30461 00323c45ea83
equal deleted inserted replaced
30432:aad3cd70e25a 30439:57c68b3af2ea
   242 now in directory HOL/Decision_Procs.
   242 now in directory HOL/Decision_Procs.
   243 
   243 
   244 * Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method
   244 * Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method
   245 "approximation".  It proves formulas on real values by using interval arithmetic.
   245 "approximation".  It proves formulas on real values by using interval arithmetic.
   246 In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
   246 In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
   247 exp and the constant pi are allowed.  For examples see HOL/ex/ApproximationEx.thy.
   247 exp and the constant pi are allowed. For examples see
       
   248 HOL/Descision_Procs/ex/Approximation_Ex.thy.
   248 
   249 
   249 * Theory "Reflection" now resides in HOL/Library.
   250 * Theory "Reflection" now resides in HOL/Library.
   250 
   251 
   251 * Entry point to Word library now simply named "Word".  INCOMPATIBILITY.
   252 * Entry point to Word library now simply named "Word".  INCOMPATIBILITY.
   252 
   253