equal
deleted
inserted
replaced
79 sources by searching for "notation=" (without quotes and no extra |
79 sources by searching for "notation=" (without quotes and no extra |
80 space). Occasional INCOMPATIBILITY for 'no_syntax' or 'no_notation' |
80 space). Occasional INCOMPATIBILITY for 'no_syntax' or 'no_notation' |
81 declarations in user applications: the mixfix template needs to be |
81 declarations in user applications: the mixfix template needs to be |
82 adapted accordingly, but it is often better to use "unbundle no |
82 adapted accordingly, but it is often better to use "unbundle no |
83 foobar_syntax", as explained for HOL libraries below. |
83 foobar_syntax", as explained for HOL libraries below. |
|
84 |
|
85 * The option "show_brackets" has been discontinued: its inaccurate |
|
86 placement of extra parentheses has been superseded by markup of mixfix |
|
87 blocks (which allows to explore subterm structure in the Prover IDE via |
|
88 C-mouse hovering). |
84 |
89 |
85 * Command "unbundle b" and its variants like "context includes b" allow |
90 * Command "unbundle b" and its variants like "context includes b" allow |
86 an optional name prefix with the reserved word "no": "unbundle no b" |
91 an optional name prefix with the reserved word "no": "unbundle no b" |
87 etc. This reverses both the order and polarity of bundled declarations |
92 etc. This reverses both the order and polarity of bundled declarations |
88 like 'notation' vs. 'no_notation', and thus avoids redundant bundle |
93 like 'notation' vs. 'no_notation', and thus avoids redundant bundle |
133 unbundle no datatype_record_syntax |
138 unbundle no datatype_record_syntax |
134 |
139 |
135 * Printing of constants and bound variables is more careful to avoid |
140 * Printing of constants and bound variables is more careful to avoid |
136 free variables, and fixed variables with mixfix syntax (including |
141 free variables, and fixed variables with mixfix syntax (including |
137 'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac". |
142 'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac". |
|
143 |
138 |
144 |
139 |
145 |
140 *** Isabelle/jEdit Prover IDE *** |
146 *** Isabelle/jEdit Prover IDE *** |
141 |
147 |
142 * Action isabelle.select_structure (with keyboard shortcut C+7) extends |
148 * Action isabelle.select_structure (with keyboard shortcut C+7) extends |