18 existing theory and ML files. |
18 existing theory and ML files. |
19 |
19 |
20 *** Isar *** |
20 *** Isar *** |
21 |
21 |
22 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac: |
22 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac: |
23 |
|
24 - Now understand static (Isar) contexts. As a consequence, users of Isar |
23 - Now understand static (Isar) contexts. As a consequence, users of Isar |
25 locales are no longer forced to write Isar proof scripts. |
24 locales are no longer forced to write Isar proof scripts. |
26 For details see Isar Reference Manual, paragraph 4.3.2: Further tactic |
25 For details see Isar Reference Manual, paragraph 4.3.2: Further tactic |
27 emulations. |
26 emulations. |
28 - INCOMPATIBILITY: names of variables to be instantiated may no |
27 - INCOMPATIBILITY: names of variables to be instantiated may no |
29 longer be enclosed in quotes. Instead, precede variable names containing |
28 longer be enclosed in quotes. Instead, precede variable name with `?'. |
30 dots with `?'. This is consistent with the instantiation attribute |
29 This is consistent with the instantiation attribute "where". |
31 "where". |
30 |
|
31 * Locales: |
|
32 - Goal statements involving the context element "includes" no longer |
|
33 generate theorems with internal delta predicates (those ending on |
|
34 "_axioms") in the premise. |
|
35 Resolve particular premise with <locale>.intro to obtain old form. |
|
36 - Fixed bug in type inference ("unify_frozen") that prevented mix of target |
|
37 specification and "includes" elements in goal statement. |
32 |
38 |
33 * HOL: Tactic emulation methods induct_tac and case_tac understand static |
39 * HOL: Tactic emulation methods induct_tac and case_tac understand static |
34 (Isar) contexts. |
40 (Isar) contexts. |
35 |
41 |
36 *** HOL *** |
42 *** HOL *** |