equal
deleted
inserted
replaced
102 interpreted in the same manner as for the 'syntax' command. |
102 interpreted in the same manner as for the 'syntax' command. |
103 |
103 |
104 * 'Advanced' translation functions (parse_translation etc.) may depend |
104 * 'Advanced' translation functions (parse_translation etc.) may depend |
105 on the signature of the theory context being presently used for |
105 on the signature of the theory context being presently used for |
106 parsing/printing, see also isar-ref manual. |
106 parsing/printing, see also isar-ref manual. |
|
107 |
|
108 * Improved 'oracle' command provides a type-safe interface to turn an |
|
109 ML expression of type theory -> T -> term into a primitive rule of |
|
110 type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle |
|
111 is already included here); see also FOL/ex/IffExample.thy; |
|
112 INCOMPATIBILITY. |
107 |
113 |
108 * Improved internal renaming of symbolic identifiers -- attach primes |
114 * Improved internal renaming of symbolic identifiers -- attach primes |
109 instead of base 26 numbers. |
115 instead of base 26 numbers. |
110 |
116 |
111 * New flag show_question_marks controls printing of leading question |
117 * New flag show_question_marks controls printing of leading question |