equal
deleted
inserted
replaced
37 * Improved support for auxiliary contexts indicate block structure for |
37 * Improved support for auxiliary contexts indicate block structure for |
38 specifications: nesting of "context fixes ... context assumes ..." |
38 specifications: nesting of "context fixes ... context assumes ..." |
39 and "class ... context ...". |
39 and "class ... context ...". |
40 |
40 |
41 * Attribute "consumes" allows a negative value as well, which is |
41 * Attribute "consumes" allows a negative value as well, which is |
42 interpreted relatively to the total number if premises of the rule in |
42 interpreted relatively to the total number of premises of the rule in |
43 the target context. This form of declaration is stable when exported |
43 the target context. This form of declaration is stable when exported |
44 from a nested 'context' with additional assumptions. It is the |
44 from a nested 'context' with additional assumptions. It is the |
45 preferred form for definitional packages, notably cases/rules produced |
45 preferred form for definitional packages, notably cases/rules produced |
46 in HOL/inductive and HOL/function. |
46 in HOL/inductive and HOL/function. |
47 |
47 |