equal
deleted
inserted
replaced
30 depend on the signature of the theory context being presently used |
30 depend on the signature of the theory context being presently used |
31 for parsing/printing, see also isar-ref manual. |
31 for parsing/printing, see also isar-ref manual. |
32 |
32 |
33 * Pure: tuned internal renaming of symbolic identifiers -- attach |
33 * Pure: tuned internal renaming of symbolic identifiers -- attach |
34 primes instead of base 26 numbers. |
34 primes instead of base 26 numbers. |
|
35 |
|
36 * Pure: clear separation of logical types and nonterminals, where the |
|
37 latter may only occur in 'syntax' specifications or type |
|
38 abbreviations. Before that distinction was only partially |
|
39 implemented via type class "logic" vs. "{}". Potential |
|
40 INCOMPATIBILITY in rare cases of improper use of 'types'/'consts' |
|
41 instead of 'nonterminals'/'syntax'. Some very exotic syntax |
|
42 specifications requiring additional non-logical non-syntactic types |
|
43 (apart from 'prop' vs. 'logic') may need to be reformulated with |
|
44 duplicated 'consts'/'syntax' declarations (e.g. see Cube/Base.thy). |
35 |
45 |
36 |
46 |
37 *** HOL *** |
47 *** HOL *** |
38 |
48 |
39 * HOL/record: reimplementation of records. Improved scalability for |
49 * HOL/record: reimplementation of records. Improved scalability for |