3 |
3 |
4 New in this Isabelle release |
4 New in this Isabelle release |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
8 |
|
9 * Pure: Simplification procedures can now take the current simpset as |
|
10 an additional argument; This is useful for calling the simplifier |
|
11 recursively. See the functions MetaSimplifier.full_{mk_simproc, |
|
12 simproc,simproc_i}. |
|
13 |
8 |
14 * Pure: considerably improved version of 'constdefs' command. Now |
9 * Pure: considerably improved version of 'constdefs' command. Now |
15 performs automatic type-inference of declared constants; additional |
10 performs automatic type-inference of declared constants; additional |
16 support for local structure declarations (cf. locales and HOL |
11 support for local structure declarations (cf. locales and HOL |
17 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |
12 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |
40 * Pure: removed obsolete type class "logic", use the top sort {} |
35 * Pure: removed obsolete type class "logic", use the top sort {} |
41 instead. Note that non-logical types should be declared as |
36 instead. Note that non-logical types should be declared as |
42 'nonterminals' rather than 'types'. INCOMPATIBILITY for new |
37 'nonterminals' rather than 'types'. INCOMPATIBILITY for new |
43 object-logic specifications. |
38 object-logic specifications. |
44 |
39 |
45 * Pure/Tactic: print_tac now outputs the goal through the trace |
40 * Pure: print_tac now outputs the goal through the trace channel. |
46 channel. |
41 |
47 |
42 * Pure: reference Namespace.unique_names included. If true the |
48 * Pure/Namespace: reference Namespace.unique_names included. |
43 (shortest) namespace-prefix is printed to disambiguate conflicts (as |
49 If true the (shortest) namespace-prefix is printed to disambiguate |
44 yet). If false the first entry wins (as during parsing). Default |
50 conflicts (as yet). If false the first entry wins (as during |
45 value is true. |
51 parsing). Default value is true. |
|
52 |
46 |
53 * Pure/Syntax: inner syntax includes (*(*nested*) comments*). |
47 * Pure/Syntax: inner syntax includes (*(*nested*) comments*). |
54 |
48 |
55 * Pure/Syntax: pretty pinter now supports unbreakable blocks, |
49 * Pure/Syntax: pretty pinter now supports unbreakable blocks, |
56 specified in mixfix annotations as "(00...)". |
50 specified in mixfix annotations as "(00...)". |
72 not require additional LaTeX packages (depending on comments in |
66 not require additional LaTeX packages (depending on comments in |
73 isabellesym.sty) are displayed properly, everything else is left |
67 isabellesym.sty) are displayed properly, everything else is left |
74 verbatim. We use isatool display and isatool print as front ends; |
68 verbatim. We use isatool display and isatool print as front ends; |
75 these are subject to the DVI_VIEWER and PRINT_COMMAND settings, |
69 these are subject to the DVI_VIEWER and PRINT_COMMAND settings, |
76 respectively. |
70 respectively. |
|
71 |
|
72 * ML: simplification procedures may now take the current simpset into |
|
73 account (cf. Simplifier.simproc(_i) / mk_simproc interface), which |
|
74 is very useful for calling the Simplifier recursively. Minor |
|
75 INCOMPATIBILITY: the 'prems' argument of simprocs is gone -- use |
|
76 prems_of_ss on the simpset instead. Moreover, the low-level |
|
77 mk_simproc no longer applies Logic.varify internally, to allow for |
|
78 use in a context of fixed variables. |
77 |
79 |
78 * ML: output via the Isabelle channels of writeln/warning/error |
80 * ML: output via the Isabelle channels of writeln/warning/error |
79 etc. is now passed through Output.output, with a hook for arbitrary |
81 etc. is now passed through Output.output, with a hook for arbitrary |
80 transformations depending on the print_mode (cf. Output.add_mode -- |
82 transformations depending on the print_mode (cf. Output.add_mode -- |
81 the first active mode that provides a output function wins). |
83 the first active mode that provides a output function wins). |
102 The top-level (users) view on records is preserved. Potential |
104 The top-level (users) view on records is preserved. Potential |
103 INCOMPATIBILITY only in strange cases, where the theory depends on |
105 INCOMPATIBILITY only in strange cases, where the theory depends on |
104 the old record representation. The type generated for a record is |
106 the old record representation. The type generated for a record is |
105 called <record_name>_ext_type. |
107 called <record_name>_ext_type. |
106 |
108 |
107 * HOL/record: Reference record_quick_and_dirty_sensitive |
109 * HOL/record: Reference record_quick_and_dirty_sensitive can be |
108 can be enabled to skip the proofs triggered by a record definition |
110 enabled to skip the proofs triggered by a record definition or a |
109 or a simproc (if quick_and_dirty is enabled). Definitions of large records can |
111 simproc (if quick_and_dirty is enabled). Definitions of large |
110 take quite long. |
112 records can take quite long. |
|
113 |
|
114 * HOL/record: "record_upd_simproc" for simplification of multiple |
|
115 record updates enabled by default. Moreover, trivial updates are |
|
116 also removed: r(|x := x r|) = r. INCOMPATIBILITY: old proofs break |
|
117 occasionally, since simplification is more powerful by default. |
111 |
118 |
112 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows: |
119 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows: |
113 |
120 |
114 syntax (epsilon) |
121 syntax (epsilon) |
115 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
122 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
116 |
123 |
117 The symbol \<some> is displayed as the alternative epsilon of LaTeX |
124 The symbol \<some> is displayed as the alternative epsilon of LaTeX |
118 and x-symbol; use option '-m epsilon' to get it actually printed. |
125 and x-symbol; use option '-m epsilon' to get it actually printed. |
119 Moreover, the mathematically important symbolic identifier |
126 Moreover, the mathematically important symbolic identifier |
120 \<epsilon> becomes available as variable, constant etc. |
127 \<epsilon> becomes available as variable, constant etc. |
121 |
|
122 * Simplifier: "record_upd_simproc" for simplification of multiple |
|
123 record updates enabled by default. Moreover trivial updates are |
|
124 also removed: r(|x := x r|) = r. |
|
125 INCOMPATIBILITY: old proofs break occasionally, since simplification |
|
126 is more powerful by default. |
|
127 |
128 |
128 |
129 |
129 *** HOLCF *** |
130 *** HOLCF *** |
130 |
131 |
131 * HOLCF: discontinued special version of 'constdefs' (which used to |
132 * HOLCF: discontinued special version of 'constdefs' (which used to |