equal
deleted
inserted
replaced
22 example and HOL/Library/Eval.thy for an ML example. |
22 example and HOL/Library/Eval.thy for an ML example. |
23 Superseedes some immature attempts. |
23 Superseedes some immature attempts. |
24 |
24 |
25 |
25 |
26 *** HOL *** |
26 *** HOL *** |
|
27 |
|
28 * New class "uminus" with operation "uminus" (split of from class "minus" |
|
29 which now only has operation "minus", binary). |
27 |
30 |
28 * New primrec package. Specification syntax conforms in style to |
31 * New primrec package. Specification syntax conforms in style to |
29 definition/function/.... No separate induction rule is provided. |
32 definition/function/.... No separate induction rule is provided. |
30 The "primrec" command distinguishes old-style and new-style specifications |
33 The "primrec" command distinguishes old-style and new-style specifications |
31 by syntax. The former primrec package is now named OldPrimrecPackage. |
34 by syntax. The former primrec package is now named OldPrimrecPackage. |