equal
deleted
inserted
replaced
243 is printed. In square brackets a particular named evaluation |
243 is printed. In square brackets a particular named evaluation |
244 mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
244 mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
245 further src/HOL/ex/Eval_Examples.thy. |
245 further src/HOL/ex/Eval_Examples.thy. |
246 |
246 |
247 * New method "sizechange" to automate termination proofs using (a |
247 * New method "sizechange" to automate termination proofs using (a |
248 modification of) the size-change principle. Requires SAT solver. |
248 modification of) the size-change principle. Requires SAT solver. See |
|
249 src/HOL/ex/Termination.thy for examples. |
249 |
250 |
250 * HOL/Orderings: class "wellorder" moved here, with explicit induction |
251 * HOL/Orderings: class "wellorder" moved here, with explicit induction |
251 rule "less_induct" as assumption. For instantiation of "wellorder" by |
252 rule "less_induct" as assumption. For instantiation of "wellorder" by |
252 means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. |
253 means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. |
253 |
254 |