5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
8 |
8 |
9 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic |
9 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic |
10 (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and |
10 (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler |
11 euler (\<a>...\<z>), are now considered normal letters, and can |
11 (\<a>...\<z>), are now considered normal letters, and can therefore |
12 therefore be used anywhere where an ASCII letter (a...zA...Z) has |
12 be used anywhere where an ASCII letter (a...zA...Z) has until |
13 until now. Similarily, the symbol digits \<zero>...\<nine> are now |
13 now. COMPATIBILITY: This obviously changes the parsing of some |
14 considered normal digits. COMPATIBILITY: This obviously changes the |
14 terms, especially where a symbol has been used as a binder, say |
15 parsing of some terms, especially where a symbol has been used as a |
15 '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed |
16 binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x |
16 as an identifier. Fix it by inserting a space around former |
17 will be parsed as an identifier. Fix it by inserting a space around |
17 symbols. Call 'isatool fixgreek' to try to fix parsing errors in |
18 former symbols. Call 'isatool fixgreek' to try to fix parsing |
18 existing theory and ML files. |
19 errors in existing theory and ML files. |
|
20 |
19 |
21 *** HOL *** |
20 *** HOL *** |
22 |
21 |
23 * 'specification' command added, allowing for definition by |
22 * 'specification' command added, allowing for definition by |
24 specification. |
23 specification. |