132 internally, to allow for use in a context of fixed variables. |
132 internally, to allow for use in a context of fixed variables. |
133 |
133 |
134 * Isar debugging: new reference Toplevel.debug; default false. Set to |
134 * Isar debugging: new reference Toplevel.debug; default false. Set to |
135 make printing of exceptions THM, TERM, TYPE and THEORY more verbose. |
135 make printing of exceptions THM, TERM, TYPE and THEORY more verbose. |
136 |
136 |
137 * Locales: |
137 * Locales: modifications regarding "includes" |
138 - "includes" disallowed in declaration of named locales (command "locale"). |
138 - "includes" disallowed in declaration of named locales (command "locale"). |
139 - Fixed parameter management in theorem generation for goals with "includes". |
139 - Fixed parameter management in theorem generation for goals with "includes". |
140 INCOMPATIBILITY: rarely, the generated theorem statement is different. |
140 INCOMPATIBILITY: rarely, the generated theorem statement is different. |
141 |
141 |
142 * Locales: new commands for the interpretation of locale expressions |
142 * Locales: locale expressions permit optional mixfix redeclaration for |
|
143 renamed parameters. |
|
144 |
|
145 * Locales: new commands for the interpretation of locale expressions |
143 in theories (interpretation) and proof contexts (interpret). These take an |
146 in theories (interpretation) and proof contexts (interpret). These take an |
144 instantiation of the locale parameters and compute proof obligations from |
147 instantiation of the locale parameters and compute proof obligations from |
145 the instantiated specification. After the obligations have been discharged, |
148 the instantiated specification. After the obligations have been discharged, |
146 the instantiated theorems of the locale are added to the theory or proof |
149 the instantiated theorems of the locale are added to the theory or proof |
147 context. Interpretation is smart in that already active interpretations |
150 context. Interpretation is smart in that already active interpretations |