equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * Simplified subscripts within identifiers, using plain \<^sub> |
|
10 instead of the second copy \<^isub> and \<^isup>. Superscripts are |
|
11 only for literal tokens within notation; explicit mixfix annotations |
|
12 for consts or fixed variables may be used as fall-back for unusual |
|
13 names. Obsolete \<twosuperior> has been expanded to \<^sup>2 in |
|
14 Isabelle/HOL. INCOMPATIBILITY, use "isabelle update_sub_sup" to |
|
15 standardize symbols as a starting point for further manual cleanup. |
|
16 The ML reference variable "legacy_isub_isup" may be set as temporary |
|
17 workaround, to make the prover accept a subset of the old identifier |
|
18 syntax. |
8 |
19 |
9 * Uniform management of "quick_and_dirty" as system option (see also |
20 * Uniform management of "quick_and_dirty" as system option (see also |
10 "isabelle options"), configuration option within the context (see also |
21 "isabelle options"), configuration option within the context (see also |
11 Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor |
22 Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor |
12 INCOMPATIBILITY, need to use more official Isabelle means to access |
23 INCOMPATIBILITY, need to use more official Isabelle means to access |