equal
deleted
inserted
replaced
64 syntax just like the Isar command 'by'. |
64 syntax just like the Isar command 'by'. |
65 |
65 |
66 |
66 |
67 *** HOL *** |
67 *** HOL *** |
68 |
68 |
69 * HOL/Main: command "value" now integrates different evaluation |
69 * Normalization by evaluation now allows non-leftlinear equations. |
|
70 Declare with attribute [code nbe]. |
|
71 |
|
72 * Command "value" now integrates different evaluation |
70 mechanisms. The result of the first successful evaluation mechanism |
73 mechanisms. The result of the first successful evaluation mechanism |
71 is printed. In square brackets a particular named evaluation |
74 is printed. In square brackets a particular named evaluation |
72 mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
75 mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
73 further src/HOL/ex/Eval_Examples.thy. |
76 further src/HOL/ex/Eval_Examples.thy. |
74 |
77 |