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 |
19 |
|
20 * Pure: Macintosh and Windows line-breaks are now allowed in theory files. |
|
21 |
20 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now |
22 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now |
21 allowed in identifiers. Similar to greek letters \<^isub> is now considered |
23 allowed in identifiers. Similar to greek letters \<^isub> is now considered |
22 a normal (but invisible) letter. For multiple letter subscripts repeat |
24 a normal (but invisible) letter. For multiple letter subscripts repeat |
23 \<^isub> like this: x\<^isub>1\<^isub>2. |
25 \<^isub> like this: x\<^isub>1\<^isub>2. |
24 |
26 |
25 * Pure: Using the functions Theory.add_finals or Theory.add_finals_i |
27 * Pure: Using new Isar command "finalconsts" (or the ML functions |
26 or the new Isar command "finalconsts", it is now possible to |
28 Theory.add_finals or Theory.add_finals_i) it is now possible to |
27 make constants "final", thereby ensuring that they are not defined |
29 declare constants "final", which prevents their being given a definition |
28 later. Useful for constants whose behaviour is fixed axiomatically |
30 later. It is useful for constants whose behaviour is fixed axiomatically |
29 rather than definitionally, such as the meta-logic connectives. |
31 rather than definitionally, such as the meta-logic connectives. |
30 |
32 |
31 *** Isar *** |
33 *** Isar *** |
32 |
34 |
33 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac: |
35 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac: |