equal
deleted
inserted
replaced
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 |