NEWS
changeset 28227 77221ee0f7b9
parent 28178 e56b8b044bef
child 28233 f14f34194f63
equal deleted inserted replaced
28226:97c530dc8aca 28227:77221ee0f7b9
    60 demanding keyword 'by' and supporting the full method expression
    60 demanding keyword 'by' and supporting the full method expression
    61 syntax just like the Isar command 'by'.
    61 syntax just like the Isar command 'by'.
    62 
    62 
    63 
    63 
    64 *** HOL ***
    64 *** HOL ***
       
    65 
       
    66 * HOL/Main: command "value" now integrates different evaluation mechanisms.
       
    67 The result of the first successful evaluation mechanism is printed.
       
    68 In square brackets a particular named evaluation mechanisms may be specified
       
    69 (currently, [SML], [code] or [nbe]).  See further HOL/ex/Eval_Examples.thy.
    65 
    70 
    66 * HOL/Orderings: class "wellorder" moved here, with explicit induction
    71 * HOL/Orderings: class "wellorder" moved here, with explicit induction
    67 rule "less_induct" as assumption.  For instantiation of "wellorder" by
    72 rule "less_induct" as assumption.  For instantiation of "wellorder" by
    68 means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
    73 means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
    69 
    74