equal
deleted
inserted
replaced
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 |