equal
deleted
inserted
replaced
116 "datatype_record_syntax" to exchange its alternative notation versus |
116 "datatype_record_syntax" to exchange its alternative notation versus |
117 regular "record_syntax". This also allows to swap record syntax later |
117 regular "record_syntax". This also allows to swap record syntax later |
118 on, notably like this: |
118 on, notably like this: |
119 |
119 |
120 unbundle no datatype_record_syntax |
120 unbundle no datatype_record_syntax |
|
121 |
|
122 * Printing of constants and bound variables is more careful to avoid |
|
123 free variables, and fixed variables with mixfix syntax (including |
|
124 'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac". |
121 |
125 |
122 |
126 |
123 *** Isabelle/jEdit Prover IDE *** |
127 *** Isabelle/jEdit Prover IDE *** |
124 |
128 |
125 * Action isabelle.select_structure (with keyboard shortcut C+7) extends |
129 * Action isabelle.select_structure (with keyboard shortcut C+7) extends |