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 sizechange principle. Requires SAT solver. 
248 modification of) the sizechange 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 