NEWS
changeset 29182 9304afad825e
parent 29162 bad036eb71c4
child 29197 6d4cb27ed19c
equal deleted inserted replaced
29181:cc177742e607 29182:9304afad825e
   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