equal
deleted
inserted
replaced
45 header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
45 header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
46 commands to be used in the same theory where defined. |
46 commands to be used in the same theory where defined. |
47 |
47 |
48 |
48 |
49 *** Pure *** |
49 *** Pure *** |
|
50 |
|
51 * Command 'definition' no longer exports the foundational "raw_def" |
|
52 into the user context. Minor INCOMPATIBILITY, may use the regular |
|
53 "def" result with attribute "abs_def" to imitate the old version. |
50 |
54 |
51 * Attribute "abs_def" turns an equation of the form "f x y == t" into |
55 * Attribute "abs_def" turns an equation of the form "f x y == t" into |
52 "f == %x y. t", which ensures that "simp" or "unfold" steps always |
56 "f == %x y. t", which ensures that "simp" or "unfold" steps always |
53 expand it. This also works for object-logic equality. (Formerly |
57 expand it. This also works for object-logic equality. (Formerly |
54 undocumented feature.) |
58 undocumented feature.) |