equal
deleted
inserted
replaced
110 specified in mixfix annotations as "(00...)". |
110 specified in mixfix annotations as "(00...)". |
111 |
111 |
112 * Pure/Syntax: 'advanced' translation functions (parse_translation |
112 * Pure/Syntax: 'advanced' translation functions (parse_translation |
113 etc.) may depend on the signature of the theory context being |
113 etc.) may depend on the signature of the theory context being |
114 presently used for parsing/printing, see also isar-ref manual. |
114 presently used for parsing/printing, see also isar-ref manual. |
|
115 |
|
116 * Pure/Simplifier: you can control the depth to which conditional rewriting |
|
117 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth Limit. |
115 |
118 |
116 * Pure/Simplifier: simplification procedures may now take the current |
119 * Pure/Simplifier: simplification procedures may now take the current |
117 simpset into account (cf. Simplifier.simproc(_i) / mk_simproc |
120 simpset into account (cf. Simplifier.simproc(_i) / mk_simproc |
118 interface), which is very useful for calling the Simplifier |
121 interface), which is very useful for calling the Simplifier |
119 recursively. Minor INCOMPATIBILITY: the 'prems' argument of |
122 recursively. Minor INCOMPATIBILITY: the 'prems' argument of |