194 *** HOL *** |
194 *** HOL *** |
195 |
195 |
196 * Auxiliary class "itself" has disappeared -- classes without any parameter |
196 * Auxiliary class "itself" has disappeared -- classes without any parameter |
197 are treated as expected by the 'class' command. |
197 are treated as expected by the 'class' command. |
198 |
198 |
199 * Theory "Reflection" now resides in HOL/Library. Common reflection examples |
199 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. |
200 (Cooper, MIR, Ferrack, Approximation) now in distinct session directory |
200 |
201 HOL/Reflection. Here Approximation provides the new proof method |
201 * Common decision procedures (Cooper, MIR, Ferrack, Approximation, Dense_Linear_Order) |
202 "approximation". It proves formulas on real values by using interval arithmetic. |
202 now in directory HOL/Decision_Procs. |
|
203 |
|
204 * Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method |
|
205 "approximation". It proves formulas on real values by using interval arithmetic. |
203 In the formulas are also the transcendental functions sin, cos, tan, atan, ln, |
206 In the formulas are also the transcendental functions sin, cos, tan, atan, ln, |
204 exp and the constant pi are allowed. For examples see |
207 exp and the constant pi are allowed. For examples see HOL/ex/ApproximationEx.thy. |
205 src/HOL/ex/ApproximationEx.thy. To reach this the Leibnitz's Series for Pi and |
208 |
206 the arcus tangens and logarithm series is now proved in Isabelle. |
209 * Theory "Reflection" now resides in HOL/Library. |
207 |
210 |
208 * Entry point to Word library now simply named "Word". INCOMPATIBILITY. |
211 * Entry point to Word library now simply named "Word". INCOMPATIBILITY. |
209 |
212 |
210 * Made source layout more coherent with logical distribution |
213 * Made source layout more coherent with logical distribution |
211 structure: |
214 structure: |
212 |
215 |
213 src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy |
216 src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy |
214 src/HOL/Library/Code_Message.thy ~> src/HOL/ |
217 src/HOL/Library/Code_Message.thy ~> src/HOL/ |
215 src/HOL/Library/Dense_Linear_Order.thy ~> src/HOL/ |
|
216 src/HOL/Library/GCD.thy ~> src/HOL/ |
218 src/HOL/Library/GCD.thy ~> src/HOL/ |
217 src/HOL/Library/Order_Relation.thy ~> src/HOL/ |
219 src/HOL/Library/Order_Relation.thy ~> src/HOL/ |
218 src/HOL/Library/Parity.thy ~> src/HOL/ |
220 src/HOL/Library/Parity.thy ~> src/HOL/ |
219 src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
221 src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
220 src/HOL/Real/ContNotDenum.thy ~> src/HOL/ |
222 src/HOL/Real/ContNotDenum.thy ~> src/HOL/ |