equal
deleted
inserted
replaced
236 * Command "value" now integrates different evaluation |
236 * Command "value" now integrates different evaluation |
237 mechanisms. The result of the first successful evaluation mechanism |
237 mechanisms. The result of the first successful evaluation mechanism |
238 is printed. In square brackets a particular named evaluation |
238 is printed. In square brackets a particular named evaluation |
239 mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
239 mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
240 further src/HOL/ex/Eval_Examples.thy. |
240 further src/HOL/ex/Eval_Examples.thy. |
|
241 |
|
242 * New method "sizechange" to automate termination proofs using (a |
|
243 modification of) the size-change principle. Requires SAT solver. |
241 |
244 |
242 * HOL/Orderings: class "wellorder" moved here, with explicit induction |
245 * HOL/Orderings: class "wellorder" moved here, with explicit induction |
243 rule "less_induct" as assumption. For instantiation of "wellorder" by |
246 rule "less_induct" as assumption. For instantiation of "wellorder" by |
244 means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. |
247 means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. |
245 |
248 |