30 * Pure: There are now sub-/superscripts that can span more than one |
30 * Pure: There are now sub-/superscripts that can span more than one |
31 character. Text between \<^bsub> and \<^esub> is set in subscript in |
31 character. Text between \<^bsub> and \<^esub> is set in subscript in |
32 PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The |
32 PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The |
33 new control characters are not identifier parts. |
33 new control characters are not identifier parts. |
34 |
34 |
35 * Pure: Control-symbols of the form \<^raw...> will literally print the |
35 * Pure: Control-symbols of the form \<^raw:...> will literally print the |
36 content of ... to the latex file instead of \isacntrl... . The ... |
36 content of ... to the latex file instead of \isacntrl... . The ... |
37 accepts all printable characters excluding the end bracket >. |
37 accepts all printable characters excluding the end bracket >. |
38 |
|
39 * Pure: Symbols may only start with one backslash: \<...>. \\<...> is no |
|
40 longer accepted by the scanner. |
|
41 |
38 |
42 * Pure: Using new Isar command "finalconsts" (or the ML functions |
39 * Pure: Using new Isar command "finalconsts" (or the ML functions |
43 Theory.add_finals or Theory.add_finals_i) it is now possible to |
40 Theory.add_finals or Theory.add_finals_i) it is now possible to |
44 declare constants "final", which prevents their being given a definition |
41 declare constants "final", which prevents their being given a definition |
45 later. It is useful for constants whose behaviour is fixed axiomatically |
42 later. It is useful for constants whose behaviour is fixed axiomatically |