14 terms, especially where a symbol has been used as a binder, say |
14 terms, especially where a symbol has been used as a binder, say |
15 '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed |
15 '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed |
16 as an identifier. Fix it by inserting a space around former |
16 as an identifier. Fix it by inserting a space around former |
17 symbols. Call 'isatool fixgreek' to try to fix parsing errors in |
17 symbols. Call 'isatool fixgreek' to try to fix parsing errors in |
18 existing theory and ML files. |
18 existing theory and ML files. |
|
19 |
|
20 *** Isar *** |
|
21 |
|
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 |
|
25 locales are no longer forced to write Isar proof scripts. |
|
26 For details see Isar Reference Manual, paragraph 4.3.2: Further tactic |
|
27 emulations. |
|
28 - INCOMPATIBILITY: names of variables to be instantiated may no |
|
29 longer be enclosed in quotes. Instead, precede variable names containing |
|
30 dots with `?'. This is consistent with the instantiation attribute |
|
31 "where". |
|
32 |
|
33 * HOL: Tactic emulation methods induct_tac and case_tac understand static |
|
34 (Isar) contexts. |
19 |
35 |
20 *** HOL *** |
36 *** HOL *** |
21 |
37 |
22 * 'specification' command added, allowing for definition by |
38 * 'specification' command added, allowing for definition by |
23 specification. |
39 specification. |