author | wenzelm |
Thu, 20 Feb 2014 16:56:51 +0100 | |
changeset 55622 | ce575c2212fc |
parent 55585 | 014138b356c4 |
child 55643 | 18fe288f6801 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
54055 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
6 |
||
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
7 |
*** General *** |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
8 |
|
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
9 |
* Document antiquotation @{url} produces markup for the given URL, |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
10 |
which results in an active hyperlink within the text. |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
11 |
|
54705 | 12 |
* Document antiquotation @{file_unchecked} is like @{file}, but does |
13 |
not check existence within the file-system. |
|
14 |
||
54732 | 15 |
* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML |
16 |
workaround in Isabelle2013-1. The prover process no longer accepts |
|
17 |
old identifier syntax with \<^isub> or \<^isup>. |
|
18 |
||
55029
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
55015
diff
changeset
|
19 |
* Syntax of document antiquotation @{rail} now uses \<newline> instead |
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
55015
diff
changeset
|
20 |
of "\\", to avoid the optical illusion of escaped backslash within |
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
55015
diff
changeset
|
21 |
string token. Minor INCOMPATIBILITY. |
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
55015
diff
changeset
|
22 |
|
55122 | 23 |
* Lexical syntax (inner and outer) supports text cartouches with |
24 |
arbitrary nesting, and without escapes of quotes etc. |
|
25 |
||
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
26 |
|
54533 | 27 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
28 |
||
29 |
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. |
|
30 |
Open text buffers take precedence over copies within the file-system. |
|
31 |
||
55536 | 32 |
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for |
33 |
auxiliary ML files. |
|
34 |
||
54688 | 35 |
* Document panel: simplied interaction where every single mouse click |
36 |
(re)opens document via desktop environment or as jEdit buffer. |
|
37 |
||
54881 | 38 |
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle / |
39 |
General") allows to specify additional print modes for the prover |
|
40 |
process, without requiring old-fashioned command-line invocation of |
|
41 |
"isabelle jedit -m MODE". |
|
42 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55315
diff
changeset
|
43 |
* New panel: Simplifier trace. Provides an interactive view of the |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55315
diff
changeset
|
44 |
simplification process, enabled by the newly-introduced |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55315
diff
changeset
|
45 |
"simplifier_trace" declaration. |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55315
diff
changeset
|
46 |
|
54533 | 47 |
|
55001 | 48 |
*** Pure *** |
49 |
||
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
50 |
* Low-level type-class commands 'classes', 'classrel', 'arities' have |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
51 |
been discontinued to avoid the danger of non-trivial axiomatization |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
52 |
that is not immediately visible. INCOMPATIBILITY, use regular |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
53 |
'instance' with proof. The required OFCLASS(...) theorem might be |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
54 |
postulated via 'axiomatization' beforehand, or the proof finished |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
55 |
trivially if the underlying class definition is made vacuous (without |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
56 |
any assumptions). See also Isabelle/ML operations |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
57 |
Axclass.axiomatize_class, Axclass.axiomatize_classrel, |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
58 |
Axclass.axiomatize_arity. |
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55316
diff
changeset
|
59 |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
60 |
* Attributes "where" and "of" allow an optional context of local |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
61 |
variables ('for' declaration): these variables become schematic in the |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
62 |
instantiated theorem. |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
63 |
|
55152 | 64 |
* Obsolete attribute "standard" has been discontinued (legacy since |
65 |
Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context |
|
66 |
where instantiations with schematic variables are intended (for |
|
67 |
declaration commands like 'lemmas' or attributes like "of"). The |
|
68 |
following temporary definition may help to port old applications: |
|
69 |
||
70 |
attribute_setup standard = |
|
71 |
"Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))" |
|
72 |
||
55001 | 73 |
* More thorough check of proof context for goal statements and |
55006 | 74 |
attributed fact expressions (concerning background theory, declared |
75 |
hyps). Potential INCOMPATIBILITY, tools need to observe standard |
|
76 |
context discipline. See also Assumption.add_assumes and the more |
|
77 |
primitive Thm.assume_hyps. |
|
55001 | 78 |
|
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
79 |
* Inner syntax token language allows regular quoted strings "..." |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
80 |
(only makes sense in practice, if outer syntax is delimited |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
81 |
differently). |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
82 |
|
55001 | 83 |
|
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset
|
84 |
*** HOL *** |
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset
|
85 |
|
55139 | 86 |
* Simproc "finite_Collect" is no longer enabled by default, due to |
87 |
spurious crashes and other surprises. Potential INCOMPATIBILITY. |
|
88 |
||
55098 | 89 |
* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL". |
90 |
The "bnf", "wrap_free_constructors", "datatype_new", "codatatype", |
|
91 |
"primrec_new", "primcorec", and "primcorecursive" command are now part of |
|
92 |
"Main". |
|
93 |
Theory renamings: |
|
94 |
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) |
|
95 |
Library/Wfrec.thy ~> Wfrec.thy |
|
96 |
Library/Zorn.thy ~> Zorn.thy |
|
97 |
Cardinals/Order_Relation.thy ~> Order_Relation.thy |
|
98 |
Library/Order_Union.thy ~> Cardinals/Order_Union.thy |
|
99 |
Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy |
|
100 |
Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy |
|
101 |
Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy |
|
102 |
Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy |
|
103 |
Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy |
|
104 |
BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy |
|
105 |
BNF/Basic_BNFs.thy ~> Basic_BNFs.thy |
|
106 |
BNF/BNF_Comp.thy ~> BNF_Comp.thy |
|
107 |
BNF/BNF_Def.thy ~> BNF_Def.thy |
|
108 |
BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy |
|
109 |
BNF/BNF_GFP.thy ~> BNF_GFP.thy |
|
110 |
BNF/BNF_LFP.thy ~> BNF_LFP.thy |
|
111 |
BNF/BNF_Util.thy ~> BNF_Util.thy |
|
112 |
BNF/Coinduction.thy ~> Coinduction.thy |
|
113 |
BNF/More_BNFs.thy ~> Library/More_BNFs.thy |
|
114 |
BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy |
|
115 |
BNF/Examples/* ~> BNF_Examples/* |
|
116 |
New theories: |
|
117 |
Wellorder_Extension.thy (split from Zorn.thy) |
|
118 |
Library/Cardinal_Notations.thy |
|
119 |
Library/BNF_Decl.thy |
|
120 |
BNF_Examples/Misc_Primcorec.thy |
|
121 |
BNF_Examples/Stream_Processor.thy |
|
55519 | 122 |
Discontinued theories: |
55098 | 123 |
BNF/BNF.thy |
124 |
BNF/Equiv_Relations_More.thy |
|
55533 | 125 |
Renamed commands: |
126 |
datatype_new_compat ~> datatype_compat |
|
127 |
primrec_new ~> primrec |
|
55519 | 128 |
wrap_free_constructors ~> free_constructors |
129 |
INCOMPATIBILITY. |
|
55098 | 130 |
|
55585 | 131 |
* Old and new (co)datatype packages: |
55425 | 132 |
* Generated constants "xxx_case" and "xxx_rec" have been renamed "case_xxx" |
55519 | 133 |
and "rec_xxx" (e.g., "prod_case" ~> "case_prod"). |
55425 | 134 |
INCOMPATIBILITY. |
135 |
||
55524
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55519
diff
changeset
|
136 |
* The types "'a list" and "'a option", their set and map functions, their |
55585 | 137 |
relators, and their selectors are now produced using the new BNF-based |
138 |
datatype package. |
|
55519 | 139 |
Renamed constants: |
140 |
Option.set ~> set_option |
|
141 |
Option.map ~> map_option |
|
55525 | 142 |
option_rel ~> rel_option |
55519 | 143 |
Renamed theorems: |
55585 | 144 |
set_def ~> set_rec[abs_def] |
55519 | 145 |
map_def ~> map_rec[abs_def] |
146 |
Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") |
|
55524
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55519
diff
changeset
|
147 |
list_all2_def ~> list_all2_iff |
55585 | 148 |
set.simps ~> set_simps (or the slightly different "list.set") |
55519 | 149 |
map.simps ~> list.map |
150 |
hd.simps ~> list.sel(1) |
|
151 |
tl.simps ~> list.sel(2-3) |
|
152 |
the.simps ~> option.sel |
|
153 |
INCOMPATIBILITY. |
|
154 |
||
55098 | 155 |
* New theory: |
156 |
Cardinals/Ordinal_Arithmetic.thy |
|
157 |
||
158 |
* Theory reorganizations: |
|
159 |
* Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy |
|
160 |
||
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
161 |
* Sledgehammer: |
55289 | 162 |
- New option: |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55289
diff
changeset
|
163 |
smt_proofs |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
164 |
- Renamed options: |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
165 |
isar_compress ~> compress_isar |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
166 |
isar_try0 ~> try0_isar |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
167 |
INCOMPATIBILITY. |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
168 |
|
55315 | 169 |
* Metis: |
170 |
- Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead. |
|
171 |
INCOMPATIBILITY. |
|
172 |
||
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
173 |
* Try0: Added 'algebra' and 'meson' to the set of proof methods. |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55152
diff
changeset
|
174 |
|
55519 | 175 |
* Command renaming: enriched_type ~> functor. INCOMPATIBILITY. |
176 |
||
55015
e33c5bd729ff
added \<newline> symbol, which is used for char/string literals in HOL;
wenzelm
parents:
55007
diff
changeset
|
177 |
* The symbol "\<newline>" may be used within char or string literals |
e33c5bd729ff
added \<newline> symbol, which is used for char/string literals in HOL;
wenzelm
parents:
55007
diff
changeset
|
178 |
to represent (Char Nibble0 NibbleA), i.e. ASCII newline. |
e33c5bd729ff
added \<newline> symbol, which is used for char/string literals in HOL;
wenzelm
parents:
55007
diff
changeset
|
179 |
|
55007
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
55006
diff
changeset
|
180 |
* Activation of Z3 now works via "z3_non_commercial" system option |
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
55006
diff
changeset
|
181 |
(without requiring restart), instead of former settings variable |
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
55006
diff
changeset
|
182 |
"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu |
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
55006
diff
changeset
|
183 |
Plugin Options / Isabelle / General. |
0c07990363a3
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
wenzelm
parents:
55006
diff
changeset
|
184 |
|
54893
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset
|
185 |
* "declare [[code abort: ...]]" replaces "code_abort ...". |
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset
|
186 |
INCOMPATIBILITY. |
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset
|
187 |
|
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset
|
188 |
* "declare [[code drop: ...]]" drops all code equations associated |
54890
cb892d835803
fundamental treatment of undefined vs. universally partial replaces code_abort
haftmann
parents:
54881
diff
changeset
|
189 |
with the given constants. |
cb892d835803
fundamental treatment of undefined vs. universally partial replaces code_abort
haftmann
parents:
54881
diff
changeset
|
190 |
|
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
191 |
* Abolished slightly odd global lattice interpretation for min/max. |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
192 |
|
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
193 |
Fact consolidations: |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
194 |
min_max.inf_assoc ~> min.assoc |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
195 |
min_max.inf_commute ~> min.commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
196 |
min_max.inf_left_commute ~> min.left_commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
197 |
min_max.inf_idem ~> min.idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
198 |
min_max.inf_left_idem ~> min.left_idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
199 |
min_max.inf_right_idem ~> min.right_idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
200 |
min_max.sup_assoc ~> max.assoc |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
201 |
min_max.sup_commute ~> max.commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
202 |
min_max.sup_left_commute ~> max.left_commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
203 |
min_max.sup_idem ~> max.idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
204 |
min_max.sup_left_idem ~> max.left_idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
205 |
min_max.sup_inf_distrib1 ~> max_min_distrib2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
206 |
min_max.sup_inf_distrib2 ~> max_min_distrib1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
207 |
min_max.inf_sup_distrib1 ~> min_max_distrib2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
208 |
min_max.inf_sup_distrib2 ~> min_max_distrib1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
209 |
min_max.distrib ~> min_max_distribs |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
210 |
min_max.inf_absorb1 ~> min.absorb1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
211 |
min_max.inf_absorb2 ~> min.absorb2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
212 |
min_max.sup_absorb1 ~> max.absorb1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
213 |
min_max.sup_absorb2 ~> max.absorb2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
214 |
min_max.le_iff_inf ~> min.absorb_iff1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
215 |
min_max.le_iff_sup ~> max.absorb_iff2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
216 |
min_max.inf_le1 ~> min.cobounded1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
217 |
min_max.inf_le2 ~> min.cobounded2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
218 |
le_maxI1, min_max.sup_ge1 ~> max.cobounded1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
219 |
le_maxI2, min_max.sup_ge2 ~> max.cobounded2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
220 |
min_max.le_infI1 ~> min.coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
221 |
min_max.le_infI2 ~> min.coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
222 |
min_max.le_supI1 ~> max.coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
223 |
min_max.le_supI2 ~> max.coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
224 |
min_max.less_infI1 ~> min.strict_coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
225 |
min_max.less_infI2 ~> min.strict_coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
226 |
min_max.less_supI1 ~> max.strict_coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
227 |
min_max.less_supI2 ~> max.strict_coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
228 |
min_max.inf_mono ~> min.mono |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
229 |
min_max.sup_mono ~> max.mono |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
230 |
min_max.le_infI, min_max.inf_greatest ~> min.boundedI |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
231 |
min_max.le_supI, min_max.sup_least ~> max.boundedI |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
232 |
min_max.le_inf_iff ~> min.bounded_iff |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
233 |
min_max.le_sup_iff ~> max.bounded_iff |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
234 |
|
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
235 |
For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc, |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
236 |
min.left_commute, min.left_idem, max.commute, max.assoc, |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
237 |
max.left_commute, max.left_idem directly. |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
238 |
|
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
239 |
For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2, |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
240 |
max.cobounded1m max.cobounded2 directly. |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
241 |
|
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
242 |
For min_ac or max_ac, prefor more general collection ac_simps. |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
243 |
|
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
244 |
INCOMPATBILITY. |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
245 |
|
54850 | 246 |
* Word library: bit representations prefer type bool over type bit. |
247 |
INCOMPATIBILITY. |
|
248 |
||
54745 | 249 |
* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin. |
54850 | 250 |
INCOMPATIBILITY. |
54745 | 251 |
|
54708 | 252 |
* Code generations are provided for make, fields, extend and truncate |
253 |
operations on records. |
|
254 |
||
54295 | 255 |
* Qualified constant names Wellfounded.acc, Wellfounded.accp. |
256 |
INCOMPATIBILITY. |
|
257 |
||
54228 | 258 |
* Fact generalization and consolidation: |
259 |
neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 |
|
260 |
INCOMPATIBILITY. |
|
261 |
||
262 |
* Purely algebraic definition of even. Fact generalization and consolidation: |
|
263 |
nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd |
|
264 |
even_zero_(nat|int) ~> even_zero |
|
265 |
INCOMPATIBILITY. |
|
54055 | 266 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
267 |
* Abolished neg_numeral. |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
268 |
* Canonical representation for minus one is "- 1". |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
269 |
* Canonical representation for other negative numbers is "- (numeral _)". |
54502 | 270 |
* When devising rule sets for number calculation, consider the |
54587 | 271 |
following canonical cases: 0, 1, numeral _, - 1, - numeral _. |
272 |
* HOLogic.dest_number also recognizes numerals in non-canonical forms |
|
54893
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset
|
273 |
like "numeral One", "- numeral One", "- 0" and even "- ... - _". |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
274 |
* Syntax for negative numerals is mere input syntax. |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
275 |
INCOMPATBILITY. |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
276 |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
277 |
* Elimination of fact duplicates: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
278 |
equals_zero_I ~> minus_unique |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
279 |
diff_eq_0_iff_eq ~> right_minus_eq |
54588 | 280 |
nat_infinite ~> infinite_UNIV_nat |
281 |
int_infinite ~> infinite_UNIV_int |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
282 |
INCOMPATIBILITY. |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
283 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
284 |
* Fact name consolidation: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
285 |
diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus |
54250 | 286 |
minus_le_self_iff ~> neg_less_eq_nonneg |
287 |
le_minus_self_iff ~> less_eq_neg_nonpos |
|
288 |
neg_less_nonneg ~> neg_less_pos |
|
289 |
less_minus_self_iff ~> less_neg_neg [simp] |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
290 |
INCOMPATIBILITY. |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
291 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
292 |
* More simplification rules on unary and binary minus: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
293 |
add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1, |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
294 |
add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2, |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
295 |
add_minus_cancel, diff_add_cancel, le_add_same_cancel1, |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
296 |
le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2, |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
297 |
minus_add_cancel, uminus_add_conv_diff. These correspondingly |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
298 |
have been taken away from fact collections algebra_simps and |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
299 |
field_simps. INCOMPATIBILITY. |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
300 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
301 |
To restore proofs, the following patterns are helpful: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
302 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
303 |
a) Arbitrary failing proof not involving "diff_def": |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
304 |
Consider simplification with algebra_simps or field_simps. |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
305 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
306 |
b) Lifting rules from addition to subtraction: |
54893
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset
|
307 |
Try with "using <rule for addition> of [... "- _" ...]" by simp". |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
308 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
309 |
c) Simplification with "diff_def": just drop "diff_def". |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
310 |
Consider simplification with algebra_simps or field_simps; |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
311 |
or the brute way with |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
312 |
"simp add: diff_conv_add_uminus del: add_uminus_conv_diff". |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
313 |
|
54264 | 314 |
* SUP and INF generalized to conditionally_complete_lattice |
315 |
||
316 |
* Theory Lubs moved HOL image to HOL-Library. It is replaced by |
|
317 |
Conditionally_Complete_Lattices. INCOMPATIBILITY. |
|
318 |
||
319 |
* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them |
|
320 |
instead of explicitly stating boundedness of sets. |
|
321 |
||
54631 | 322 |
* ccpo.admissible quantifies only over non-empty chains to allow |
323 |
more syntax-directed proof rules; the case of the empty chain |
|
324 |
shows up as additional case in fixpoint induction proofs. |
|
325 |
INCOMPATIBILITY |
|
54264 | 326 |
|
55049 | 327 |
* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. |
328 |
||
54672
748778ac0ab8
relocate NEWS to post-release version (cf. 7a14f831d02d);
wenzelm
parents:
54671
diff
changeset
|
329 |
* Nitpick: |
748778ac0ab8
relocate NEWS to post-release version (cf. 7a14f831d02d);
wenzelm
parents:
54671
diff
changeset
|
330 |
- Fixed soundness bug whereby mutually recursive datatypes could take |
748778ac0ab8
relocate NEWS to post-release version (cf. 7a14f831d02d);
wenzelm
parents:
54671
diff
changeset
|
331 |
infinite values. |
748778ac0ab8
relocate NEWS to post-release version (cf. 7a14f831d02d);
wenzelm
parents:
54671
diff
changeset
|
332 |
|
54787 | 333 |
* HOL-Multivariate_Analysis: |
334 |
- type class ordered_real_vector for ordered vector spaces |
|
335 |
- changed order of ordered_euclidean_space to be compatible with |
|
336 |
pointwise ordering on products. Therefore instance of |
|
337 |
conditionally_complete_lattice and ordered_real_vector. |
|
338 |
INCOMPATIBILITY: use box instead of greaterThanLessThan or |
|
339 |
explicit set-comprehensions with eucl_less for other (half-) open |
|
340 |
intervals. |
|
341 |
||
54672
748778ac0ab8
relocate NEWS to post-release version (cf. 7a14f831d02d);
wenzelm
parents:
54671
diff
changeset
|
342 |
|
55622
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
343 |
*** Scala *** |
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
344 |
|
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
345 |
* The signature and semantics of Document.Snapshot.cumulate_markup / |
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
346 |
select_markup have been clarified. Markup is now traversed in the |
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
347 |
order of reports given by the prover: later markup is usually more |
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
348 |
specific and may override results accumulated so far. The elements |
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
349 |
guard is mandatory and checked precisely. Subtle INCOMPATIBILITY. |
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
350 |
|
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
351 |
|
54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
352 |
*** ML *** |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
353 |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
354 |
* Proper context discipline for read_instantiate and instantiate_tac: |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
355 |
variables that are meant to become schematic need to be given as |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
356 |
fixed, and are generalized by the explicit context of local variables. |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
357 |
This corresponds to Isar attributes "where" and "of" with 'for' |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
358 |
declaration. INCOMPATIBILITY, also due to potential change of indices |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
359 |
of schematic variables. |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
360 |
|
54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
361 |
* Toplevel function "use" refers to raw ML bootstrap environment, |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
362 |
without Isar context nor antiquotations. Potential INCOMPATIBILITY. |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
363 |
Note that 'ML_file' is the canonical command to load ML files into the |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
364 |
formal context. |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
365 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54732
diff
changeset
|
366 |
* Proper context for basic Simplifier operations: rewrite_rule, |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54732
diff
changeset
|
367 |
rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54732
diff
changeset
|
368 |
pass runtime Proof.context (and ensure that the simplified entity |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54732
diff
changeset
|
369 |
actually belongs to it). |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54732
diff
changeset
|
370 |
|
55547
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
55536
diff
changeset
|
371 |
* Subtle change of semantics of Thm.eq_thm: theory stamps are not |
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
55536
diff
changeset
|
372 |
compared (according to Thm.thm_ord), but assumed to be covered by the |
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
55536
diff
changeset
|
373 |
current background theory. Thus equivalent data produced in different |
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
55536
diff
changeset
|
374 |
branches of the theory graph usually coincides (e.g. relevant for |
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
55536
diff
changeset
|
375 |
theory merge). Note that the softer Thm.eq_thm_prop is often more |
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
55536
diff
changeset
|
376 |
appropriate than Thm.eq_thm. |
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
55536
diff
changeset
|
377 |
|
54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
378 |
|
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
379 |
*** System *** |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
380 |
|
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
381 |
* Simplified "isabelle display" tool. Settings variables DVI_VIEWER |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
382 |
and PDF_VIEWER now refer to the actual programs, not shell |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
383 |
command-lines. Discontinued option -c: invocation may be asynchronous |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
384 |
via desktop environment, without any special precautions. Potential |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
385 |
INCOMPATIBILITY with ambitious private settings. |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
386 |
|
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
387 |
* Improved 'display_drafts' concerning desktop integration and |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
388 |
repeated invocation in PIDE front-end: re-use single file |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
389 |
$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views. |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
390 |
|
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
391 |
|
54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
392 |
|
54639 | 393 |
New in Isabelle2013-2 (December 2013) |
394 |
------------------------------------- |
|
395 |
||
396 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
|
397 |
||
398 |
* More robust editing of running commands with internal forks, |
|
399 |
e.g. non-terminating 'by' steps. |
|
400 |
||
54641 | 401 |
* More relaxed Sledgehammer panel: avoid repeated application of query |
402 |
after edits surrounding the command location. |
|
403 |
||
54648 | 404 |
* More status information about commands that are interrupted |
405 |
accidentally (via physical event or Poly/ML runtime system signal, |
|
406 |
e.g. out-of-memory). |
|
407 |
||
54653 | 408 |
|
409 |
*** System *** |
|
410 |
||
411 |
* More robust termination of external processes managed by |
|
54664 | 412 |
Isabelle/ML: support cancellation of tasks within the range of |
413 |
milliseconds, as required for PIDE document editing with automatically |
|
414 |
tried tools (e.g. Sledgehammer). |
|
54653 | 415 |
|
54648 | 416 |
* Reactivated Isabelle/Scala kill command for external processes on |
417 |
Mac OS X, which was accidentally broken in Isabelle2013-1 due to a |
|
418 |
workaround for some Debian/Ubuntu Linux versions from 2013. |
|
419 |
||
54639 | 420 |
|
421 |
||
53971 | 422 |
New in Isabelle2013-1 (November 2013) |
423 |
------------------------------------- |
|
50994 | 424 |
|
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
425 |
*** General *** |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
426 |
|
53971 | 427 |
* Discontinued obsolete 'uses' within theory header. Note that |
428 |
commands like 'ML_file' work without separate declaration of file |
|
429 |
dependencies. Minor INCOMPATIBILITY. |
|
430 |
||
431 |
* Discontinued redundant 'use' command, which was superseded by |
|
432 |
'ML_file' in Isabelle2013. Minor INCOMPATIBILITY. |
|
433 |
||
53016
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
434 |
* Simplified subscripts within identifiers, using plain \<^sub> |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
435 |
instead of the second copy \<^isub> and \<^isup>. Superscripts are |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
436 |
only for literal tokens within notation; explicit mixfix annotations |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
437 |
for consts or fixed variables may be used as fall-back for unusual |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
438 |
names. Obsolete \<twosuperior> has been expanded to \<^sup>2 in |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
439 |
Isabelle/HOL. INCOMPATIBILITY, use "isabelle update_sub_sup" to |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
440 |
standardize symbols as a starting point for further manual cleanup. |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
441 |
The ML reference variable "legacy_isub_isup" may be set as temporary |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
442 |
workaround, to make the prover accept a subset of the old identifier |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
443 |
syntax. |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
444 |
|
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
53016
diff
changeset
|
445 |
* Document antiquotations: term style "isub" has been renamed to |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
53016
diff
changeset
|
446 |
"sub". Minor INCOMPATIBILITY. |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
53016
diff
changeset
|
447 |
|
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
448 |
* Uniform management of "quick_and_dirty" as system option (see also |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
449 |
"isabelle options"), configuration option within the context (see also |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
450 |
Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
451 |
INCOMPATIBILITY, need to use more official Isabelle means to access |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
452 |
quick_and_dirty, instead of historical poking into mutable reference. |
52059 | 453 |
|
52060 | 454 |
* Renamed command 'print_configs' to 'print_options'. Minor |
455 |
INCOMPATIBILITY. |
|
456 |
||
52430 | 457 |
* Proper diagnostic command 'print_state'. Old 'pr' (with its |
458 |
implicit change of some global references) is retained for now as |
|
459 |
control command, e.g. for ProofGeneral 3.7.x. |
|
460 |
||
52549 | 461 |
* Discontinued 'print_drafts' command with its old-fashioned PS output |
462 |
and Unix command-line print spooling. Minor INCOMPATIBILITY: use |
|
463 |
'display_drafts' instead and print via the regular document viewer. |
|
464 |
||
53971 | 465 |
* Updated and extended "isar-ref" and "implementation" manual, |
466 |
eliminated old "ref" manual. |
|
467 |
||
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
468 |
|
51533 | 469 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
470 |
||
53971 | 471 |
* New manual "jedit" for Isabelle/jEdit, see isabelle doc or |
53852 | 472 |
Documentation panel. |
473 |
||
53971 | 474 |
* Dockable window "Documentation" provides access to Isabelle |
475 |
documentation. |
|
52646 | 476 |
|
52949 | 477 |
* Dockable window "Find" provides query operations for formal entities |
478 |
(GUI front-end to 'find_theorems' command). |
|
479 |
||
53050 | 480 |
* Dockable window "Sledgehammer" manages asynchronous / parallel |
481 |
sledgehammer runs over existing document sources, independently of |
|
482 |
normal editing and checking process. |
|
483 |
||
51533 | 484 |
* Dockable window "Timing" provides an overview of relevant command |
54332 | 485 |
timing information, depending on option jedit_timing_threshold. The |
486 |
same timing information is shown in the extended tooltip of the |
|
487 |
command keyword, when hovering the mouse over it while the CONTROL or |
|
488 |
COMMAND modifier is pressed. |
|
51533 | 489 |
|
53971 | 490 |
* Improved dockable window "Theories": Continuous checking of proof |
491 |
document (visible and required parts) may be controlled explicitly, |
|
492 |
using check box or shortcut "C+e ENTER". Individual theory nodes may |
|
493 |
be marked explicitly as required and checked in full, using check box |
|
494 |
or shortcut "C+e SPACE". |
|
495 |
||
54305 | 496 |
* Improved completion mechanism, which is now managed by the |
497 |
Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle |
|
498 |
symbol abbreviations (see $ISABELLE_HOME/etc/symbols). |
|
499 |
||
54319 | 500 |
* Standard jEdit keyboard shortcut C+b complete-word is remapped to |
501 |
isabelle.complete for explicit completion in Isabelle sources. |
|
502 |
INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts |
|
503 |
to resolve conflict. |
|
504 |
||
54305 | 505 |
* Improved support of various "minor modes" for Isabelle NEWS, |
506 |
options, session ROOT etc., with completion and SideKick tree view. |
|
507 |
||
53971 | 508 |
* Strictly monotonic document update, without premature cancellation of |
509 |
running transactions that are still needed: avoid reset/restart of |
|
510 |
such command executions while editing. |
|
53271
0460d6962ced
GTK+ works better due to avoidance of default list view popups;
wenzelm
parents:
53251
diff
changeset
|
511 |
|
53971 | 512 |
* Support for asynchronous print functions, as overlay to existing |
513 |
document content. |
|
514 |
||
515 |
* Support for automatic tools in HOL, which try to prove or disprove |
|
516 |
toplevel theorem statements. |
|
517 |
||
518 |
* Action isabelle.reset-font-size resets main text area font size |
|
54365
5d45c985974a
no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;
wenzelm
parents:
54351
diff
changeset
|
519 |
according to Isabelle/Scala plugin option "jedit_font_reset_size" (see |
5d45c985974a
no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;
wenzelm
parents:
54351
diff
changeset
|
520 |
also "Plugin Options / Isabelle / General"). It can be bound to some |
5d45c985974a
no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;
wenzelm
parents:
54351
diff
changeset
|
521 |
keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0). |
53971 | 522 |
|
523 |
* File specifications in jEdit (e.g. file browser) may refer to |
|
54351 | 524 |
$ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms. Discontinued |
525 |
obsolete $ISABELLE_HOME_WINDOWS variable. |
|
53971 | 526 |
|
527 |
* Improved support for Linux look-and-feel "GTK+", see also "Utilities |
|
528 |
/ Global Options / Appearance". |
|
529 |
||
530 |
* Improved support of native Mac OS X functionality via "MacOSX" |
|
531 |
plugin, which is now enabled by default. |
|
532 |
||
51533 | 533 |
|
51313 | 534 |
*** Pure *** |
535 |
||
54049 | 536 |
* Commands 'interpretation' and 'sublocale' are now target-sensitive. |
537 |
In particular, 'interpretation' allows for non-persistent |
|
538 |
interpretation within "context ... begin ... end" blocks offering a |
|
539 |
light-weight alternative to 'sublocale'. See "isar-ref" manual for |
|
540 |
details. |
|
51747 | 541 |
|
51565 | 542 |
* Improved locales diagnostic command 'print_dependencies'. |
543 |
||
51313 | 544 |
* Discontinued obsolete 'axioms' command, which has been marked as |
545 |
legacy since Isabelle2009-2. INCOMPATIBILITY, use 'axiomatization' |
|
546 |
instead, while observing its uniform scope for polymorphism. |
|
547 |
||
51316
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
548 |
* Discontinued empty name bindings in 'axiomatization'. |
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
549 |
INCOMPATIBILITY. |
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
550 |
|
53971 | 551 |
* System option "proofs" has been discontinued. Instead the global |
552 |
state of Proofterm.proofs is persistently compiled into logic images |
|
553 |
as required, notably HOL-Proofs. Users no longer need to change |
|
554 |
Proofterm.proofs dynamically. Minor INCOMPATIBILITY. |
|
555 |
||
556 |
* Syntax translation functions (print_translation etc.) always depend |
|
557 |
on Proof.context. Discontinued former "(advanced)" option -- this is |
|
558 |
now the default. Minor INCOMPATIBILITY. |
|
559 |
||
560 |
* Former global reference trace_unify_fail is now available as |
|
561 |
configuration option "unify_trace_failure" (global context only). |
|
562 |
||
52463 | 563 |
* SELECT_GOAL now retains the syntactic context of the overall goal |
564 |
state (schematic variables etc.). Potential INCOMPATIBILITY in rare |
|
565 |
situations. |
|
566 |
||
51313 | 567 |
|
51002
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
568 |
*** HOL *** |
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
569 |
|
54032 | 570 |
* Stronger precedence of syntax for big intersection and union on |
571 |
sets, in accordance with corresponding lattice operations. |
|
572 |
INCOMPATIBILITY. |
|
573 |
||
574 |
* Notation "{p:A. P}" now allows tuple patterns as well. |
|
575 |
||
576 |
* Nested case expressions are now translated in a separate check phase |
|
577 |
rather than during parsing. The data for case combinators is separated |
|
578 |
from the datatype package. The declaration attribute |
|
579 |
"case_translation" can be used to register new case combinators: |
|
580 |
||
581 |
declare [[case_translation case_combinator constructor1 ... constructorN]] |
|
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52550
diff
changeset
|
582 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
583 |
* Code generator: |
53160 | 584 |
- 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / |
585 |
'code_instance'. |
|
586 |
- 'code_identifier' declares name hints for arbitrary identifiers in |
|
587 |
generated code, subsuming 'code_modulename'. |
|
53983 | 588 |
|
589 |
See the isar-ref manual for syntax diagrams, and the HOL theories for |
|
590 |
examples. |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
591 |
|
54032 | 592 |
* Attibute 'code': 'code' now declares concrete and abstract code |
593 |
equations uniformly. Use explicit 'code equation' and 'code abstract' |
|
594 |
to distinguish both when desired. |
|
595 |
||
596 |
* Discontinued theories Code_Integer and Efficient_Nat by a more |
|
597 |
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat, |
|
598 |
Code_Target_Nat and Code_Target_Numeral. See the tutorial on code |
|
599 |
generation for details. INCOMPATIBILITY. |
|
600 |
||
601 |
* Numeric types are mapped by default to target language numerals: |
|
602 |
natural (replaces former code_numeral) and integer (replaces former |
|
603 |
code_int). Conversions are available as integer_of_natural / |
|
604 |
natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and |
|
605 |
Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in |
|
606 |
ML). INCOMPATIBILITY. |
|
607 |
||
608 |
* Function package: For mutually recursive functions f and g, separate |
|
609 |
cases rules f.cases and g.cases are generated instead of unusable |
|
610 |
f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY, |
|
611 |
in the case that the unusable rule was used nevertheless. |
|
612 |
||
613 |
* Function package: For each function f, new rules f.elims are |
|
614 |
generated, which eliminate equalities of the form "f x = t". |
|
615 |
||
616 |
* New command 'fun_cases' derives ad-hoc elimination rules for |
|
617 |
function equations as simplified instances of f.elims, analogous to |
|
618 |
inductive_cases. See ~~/src/HOL/ex/Fundefs.thy for some examples. |
|
53307 | 619 |
|
54021 | 620 |
* Lifting: |
621 |
- parametrized correspondence relations are now supported: |
|
54378 | 622 |
+ parametricity theorems for the raw term can be specified in |
54021 | 623 |
the command lift_definition, which allow us to generate stronger |
624 |
transfer rules |
|
625 |
+ setup_lifting generates stronger transfer rules if parametric |
|
626 |
correspondence relation can be generated |
|
627 |
+ various new properties of the relator must be specified to support |
|
628 |
parametricity |
|
629 |
+ parametricity theorem for the Quotient relation can be specified |
|
630 |
- setup_lifting generates domain rules for the Transfer package |
|
631 |
- stronger reflexivity prover of respectfulness theorems for type |
|
632 |
copies |
|
633 |
- ===> and --> are now local. The symbols can be introduced |
|
634 |
by interpreting the locale lifting_syntax (typically in an |
|
635 |
anonymous context) |
|
54378 | 636 |
- Lifting/Transfer relevant parts of Library/Quotient_* are now in |
54021 | 637 |
Main. Potential INCOMPATIBILITY |
638 |
- new commands for restoring and deleting Lifting/Transfer context: |
|
639 |
lifting_forget, lifting_update |
|
54378 | 640 |
- the command print_quotmaps was renamed to print_quot_maps. |
54021 | 641 |
INCOMPATIBILITY |
642 |
||
643 |
* Transfer: |
|
54378 | 644 |
- better support for domains in Transfer: replace Domainp T |
54021 | 645 |
by the actual invariant in a transferred goal |
646 |
- transfer rules can have as assumptions other transfer rules |
|
647 |
- Experimental support for transferring from the raw level to the |
|
648 |
abstract level: Transfer.transferred attribute |
|
649 |
- Attribute version of the transfer method: untransferred attribute |
|
650 |
||
52286 | 651 |
* Reification and reflection: |
53160 | 652 |
- Reification is now directly available in HOL-Main in structure |
653 |
"Reification". |
|
654 |
- Reflection now handles multiple lists with variables also. |
|
655 |
- The whole reflection stack has been decomposed into conversions. |
|
52286 | 656 |
INCOMPATIBILITY. |
657 |
||
51489 | 658 |
* Revised devices for recursive definitions over finite sets: |
659 |
- Only one fundamental fold combinator on finite set remains: |
|
660 |
Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b |
|
661 |
This is now identity on infinite sets. |
|
52745
821ce370b7fc
avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
wenzelm
parents:
52743
diff
changeset
|
662 |
- Locales ("mini packages") for fundamental definitions with |
51489 | 663 |
Finite_Set.fold: folding, folding_idem. |
664 |
- Locales comm_monoid_set, semilattice_order_set and |
|
665 |
semilattice_neutr_order_set for big operators on sets. |
|
666 |
See theory Big_Operators for canonical examples. |
|
667 |
Note that foundational constants comm_monoid_set.F and |
|
668 |
semilattice_set.F correspond to former combinators fold_image |
|
669 |
and fold1 respectively. These are now gone. You may use |
|
51490 | 670 |
those foundational constants as substitutes, but it is |
53983 | 671 |
preferable to interpret the above locales accordingly. |
51489 | 672 |
- Dropped class ab_semigroup_idem_mult (special case of lattice, |
673 |
no longer needed in connection with Finite_Set.fold etc.) |
|
674 |
- Fact renames: |
|
675 |
card.union_inter ~> card_Un_Int [symmetric] |
|
676 |
card.union_disjoint ~> card_Un_disjoint |
|
677 |
INCOMPATIBILITY. |
|
678 |
||
51487 | 679 |
* Locale hierarchy for abstract orderings and (semi)lattices. |
680 |
||
53526 | 681 |
* Complete_Partial_Order.admissible is defined outside the type class |
682 |
ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the |
|
683 |
class predicate assumption or sort constraint when possible. |
|
53362 | 684 |
INCOMPATIBILITY. |
685 |
||
53160 | 686 |
* Introduce type class "conditionally_complete_lattice": Like a |
687 |
complete lattice but does not assume the existence of the top and |
|
688 |
bottom elements. Allows to generalize some lemmas about reals and |
|
689 |
extended reals. Removed SupInf and replaced it by the instantiation |
|
690 |
of conditionally_complete_lattice for real. Renamed lemmas about |
|
691 |
conditionally-complete lattice from Sup_... to cSup_... and from |
|
692 |
Inf_... to cInf_... to avoid hidding of similar complete lattice |
|
693 |
lemmas. |
|
694 |
||
695 |
* Introduce type class linear_continuum as combination of |
|
696 |
conditionally-complete lattices and inner dense linorders which have |
|
697 |
more than one element. INCOMPATIBILITY. |
|
698 |
||
53983 | 699 |
* Introduced type classes order_top and order_bot. The old classes top |
700 |
and bot only contain the syntax without assumptions. INCOMPATIBILITY: |
|
701 |
Rename bot -> order_bot, top -> order_top |
|
53683 | 702 |
|
53160 | 703 |
* Introduce type classes "no_top" and "no_bot" for orderings without |
704 |
top and bottom elements. |
|
51732 | 705 |
|
706 |
* Split dense_linorder into inner_dense_order and no_top, no_bot. |
|
707 |
||
708 |
* Complex_Main: Unify and move various concepts from |
|
53160 | 709 |
HOL-Multivariate_Analysis to HOL-Complex_Main. |
51732 | 710 |
|
53983 | 711 |
- Introduce type class (lin)order_topology and |
712 |
linear_continuum_topology. Allows to generalize theorems about |
|
713 |
limits and order. Instances are reals and extended reals. |
|
51732 | 714 |
|
715 |
- continuous and continuos_on from Multivariate_Analysis: |
|
53983 | 716 |
"continuous" is the continuity of a function at a filter. "isCont" |
717 |
is now an abbrevitation: "isCont x f == continuous (at _) f". |
|
718 |
||
719 |
Generalized continuity lemmas from isCont to continuous on an |
|
720 |
arbitrary filter. |
|
721 |
||
722 |
- compact from Multivariate_Analysis. Use Bolzano's lemma to prove |
|
723 |
compactness of closed intervals on reals. Continuous functions |
|
724 |
attain infimum and supremum on compact sets. The inverse of a |
|
725 |
continuous function is continuous, when the function is continuous |
|
726 |
on a compact set. |
|
51732 | 727 |
|
728 |
- connected from Multivariate_Analysis. Use it to prove the |
|
51775
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
729 |
intermediate value theorem. Show connectedness of intervals on |
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
730 |
linear_continuum_topology). |
51732 | 731 |
|
732 |
- first_countable_topology from Multivariate_Analysis. Is used to |
|
53983 | 733 |
show equivalence of properties on the neighbourhood filter of x and |
734 |
on all sequences converging to x. |
|
735 |
||
736 |
- FDERIV: Definition of has_derivative moved to Deriv.thy. Moved |
|
737 |
theorems from Library/FDERIV.thy to Deriv.thy and base the |
|
738 |
definition of DERIV on FDERIV. Add variants of DERIV and FDERIV |
|
739 |
which are restricted to sets, i.e. to represent derivatives from |
|
740 |
left or right. |
|
51732 | 741 |
|
742 |
- Removed the within-filter. It is replaced by the principal filter: |
|
743 |
||
744 |
F within X = inf F (principal X) |
|
745 |
||
746 |
- Introduce "at x within U" as a single constant, "at x" is now an |
|
747 |
abbreviation for "at x within UNIV" |
|
748 |
||
53983 | 749 |
- Introduce named theorem collections tendsto_intros, |
750 |
continuous_intros, continuous_on_intros and FDERIV_intros. Theorems |
|
751 |
in tendsto_intros (or FDERIV_intros) are also available as |
|
752 |
tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side |
|
753 |
is replaced by a congruence rule. This allows to apply them as |
|
754 |
intro rules and then proving equivalence by the simplifier. |
|
51732 | 755 |
|
756 |
- Restructured theories in HOL-Complex_Main: |
|
757 |
||
758 |
+ Moved RealDef and RComplete into Real |
|
759 |
||
760 |
+ Introduced Topological_Spaces and moved theorems about |
|
761 |
topological spaces, filters, limits and continuity to it |
|
762 |
||
763 |
+ Renamed RealVector to Real_Vector_Spaces |
|
764 |
||
53983 | 765 |
+ Split Lim, SEQ, Series into Topological_Spaces, |
766 |
Real_Vector_Spaces, and Limits |
|
51732 | 767 |
|
768 |
+ Moved Ln and Log to Transcendental |
|
769 |
||
770 |
+ Moved theorems about continuity from Deriv to Topological_Spaces |
|
771 |
||
772 |
- Remove various auxiliary lemmas. |
|
773 |
||
774 |
INCOMPATIBILITY. |
|
51002
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
775 |
|
53738 | 776 |
* Nitpick: |
53803 | 777 |
- Added option "spy" |
53738 | 778 |
- Reduce incidence of "too high arity" errors |
779 |
||
51137 | 780 |
* Sledgehammer: |
781 |
- Renamed option: |
|
782 |
isar_shrink ~> isar_compress |
|
53738 | 783 |
INCOMPATIBILITY. |
53801 | 784 |
- Added options "isar_try0", "spy" |
53728 | 785 |
- Better support for "isar_proofs" |
53766 | 786 |
- MaSh has been fined-tuned and now runs as a local server |
51137 | 787 |
|
54032 | 788 |
* Improved support for ad hoc overloading of constants (see also |
789 |
isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy). |
|
790 |
||
791 |
* Library/Polynomial.thy: |
|
792 |
- Use lifting for primitive definitions. |
|
793 |
- Explicit conversions from and to lists of coefficients, used for |
|
794 |
generated code. |
|
795 |
- Replaced recursion operator poly_rec by fold_coeffs. |
|
796 |
- Prefer pre-existing gcd operation for gcd. |
|
797 |
- Fact renames: |
|
798 |
poly_eq_iff ~> poly_eq_poly_eq_iff |
|
799 |
poly_ext ~> poly_eqI |
|
800 |
expand_poly_eq ~> poly_eq_iff |
|
801 |
IMCOMPATIBILITY. |
|
802 |
||
803 |
* New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and |
|
804 |
case_of_simps to convert function definitions between a list of |
|
805 |
equations with patterns on the lhs and a single equation with case |
|
806 |
expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy. |
|
807 |
||
808 |
* New Library/FSet.thy: type of finite sets defined as a subtype of |
|
809 |
sets defined by Lifting/Transfer. |
|
810 |
||
811 |
* Discontinued theory src/HOL/Library/Eval_Witness. INCOMPATIBILITY. |
|
812 |
||
813 |
* Consolidation of library theories on product orders: |
|
814 |
||
815 |
Product_Lattice ~> Product_Order -- pointwise order on products |
|
816 |
Product_ord ~> Product_Lexorder -- lexicographic order on products |
|
817 |
||
818 |
INCOMPATIBILITY. |
|
819 |
||
53160 | 820 |
* Imperative-HOL: The MREC combinator is considered legacy and no |
821 |
longer included by default. INCOMPATIBILITY, use partial_function |
|
822 |
instead, or import theory Legacy_Mrec as a fallback. |
|
823 |
||
53983 | 824 |
* HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and |
825 |
~~/src/HOL/Algebra/poly. Existing theories should be based on |
|
826 |
~~/src/HOL/Library/Polynomial instead. The latter provides |
|
827 |
integration with HOL's type classes for rings. INCOMPATIBILITY. |
|
51517
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
828 |
|
54033 | 829 |
* HOL-BNF: |
54032 | 830 |
- Various improvements to BNF-based (co)datatype package, including |
831 |
new commands "primrec_new", "primcorec", and |
|
832 |
"datatype_new_compat", as well as documentation. See |
|
833 |
"datatypes.pdf" for details. |
|
834 |
- New "coinduction" method to avoid some boilerplate (compared to |
|
835 |
coinduct). |
|
836 |
- Renamed keywords: |
|
837 |
data ~> datatype_new |
|
838 |
codata ~> codatatype |
|
839 |
bnf_def ~> bnf |
|
840 |
- Renamed many generated theorems, including |
|
841 |
discs ~> disc |
|
842 |
map_comp' ~> map_comp |
|
843 |
map_id' ~> map_id |
|
844 |
sels ~> sel |
|
845 |
set_map' ~> set_map |
|
846 |
sets ~> set |
|
847 |
IMCOMPATIBILITY. |
|
848 |
||
51517
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
849 |
|
51551 | 850 |
*** ML *** |
851 |
||
53971 | 852 |
* Spec_Check is a Quickcheck tool for Isabelle/ML. The ML function |
853 |
"check_property" allows to check specifications of the form "ALL x y |
|
854 |
z. prop x y z". See also ~~/src/Tools/Spec_Check/ with its |
|
855 |
Examples.thy in particular. |
|
856 |
||
53709
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
53683
diff
changeset
|
857 |
* Improved printing of exception trace in Poly/ML 5.5.1, with regular |
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
53683
diff
changeset
|
858 |
tracing output in the command transaction context instead of physical |
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
53683
diff
changeset
|
859 |
stdout. See also Toplevel.debug, Toplevel.debugging and |
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
53683
diff
changeset
|
860 |
ML_Compiler.exn_trace. |
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
53683
diff
changeset
|
861 |
|
53971 | 862 |
* ML type "theory" is now immutable, without any special treatment of |
863 |
drafts or linear updates (which could lead to "stale theory" errors in |
|
864 |
the past). Discontinued obsolete operations like Theory.copy, |
|
865 |
Theory.checkpoint, and the auxiliary type theory_ref. Minor |
|
866 |
INCOMPATIBILITY. |
|
53164
beb4ee344c22
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
wenzelm
parents:
53162
diff
changeset
|
867 |
|
51551 | 868 |
* More uniform naming of goal functions for skipped proofs: |
869 |
||
870 |
Skip_Proof.prove ~> Goal.prove_sorry |
|
871 |
Skip_Proof.prove_global ~> Goal.prove_sorry_global |
|
872 |
||
53971 | 873 |
Minor INCOMPATIBILITY. |
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51689
diff
changeset
|
874 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
875 |
* Simplifier tactics and tools use proper Proof.context instead of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
876 |
historic type simpset. Old-style declarations like addsimps, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
877 |
addsimprocs etc. operate directly on Proof.context. Raw type simpset |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
878 |
retains its use as snapshot of the main Simplifier context, using |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
879 |
simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
880 |
old tools by making them depend on (ctxt : Proof.context) instead of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
881 |
(ss : simpset), then turn (simpset_of ctxt) into ctxt. |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
882 |
|
53971 | 883 |
* Modifiers for classical wrappers (e.g. addWrapper, delWrapper) |
884 |
operate on Proof.context instead of claset, for uniformity with addIs, |
|
885 |
addEs, addDs etc. Note that claset_of and put_claset allow to manage |
|
886 |
clasets separately from the context. |
|
887 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
888 |
* Discontinued obsolete ML antiquotations @{claset} and @{simpset}. |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
889 |
INCOMPATIBILITY, use @{context} instead. |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
890 |
|
53971 | 891 |
* Antiquotation @{theory_context A} is similar to @{theory A}, but |
892 |
presents the result as initial Proof.context. |
|
893 |
||
51551 | 894 |
|
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
895 |
*** System *** |
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
896 |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
51775
diff
changeset
|
897 |
* Discontinued obsolete isabelle usedir, mkdir, make -- superseded by |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
51775
diff
changeset
|
898 |
"isabelle build" in Isabelle2013. INCOMPATIBILITY. |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
899 |
|
52054
eaf17514aabd
discontinued obsolete isabelle-process options -f and -u;
wenzelm
parents:
52053
diff
changeset
|
900 |
* Discontinued obsolete isabelle-process options -f and -u (former |
eaf17514aabd
discontinued obsolete isabelle-process options -f and -u;
wenzelm
parents:
52053
diff
changeset
|
901 |
administrative aliases of option -e). Minor INCOMPATIBILITY. |
eaf17514aabd
discontinued obsolete isabelle-process options -f and -u;
wenzelm
parents:
52053
diff
changeset
|
902 |
|
52550 | 903 |
* Discontinued obsolete isabelle print tool, and PRINT_COMMAND |
904 |
settings variable. |
|
905 |
||
52746 | 906 |
* Discontinued ISABELLE_DOC_FORMAT settings variable and historic |
907 |
document formats: dvi.gz, ps, ps.gz -- the default document format is |
|
908 |
always pdf. |
|
52743 | 909 |
|
52053 | 910 |
* Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to |
911 |
specify global resources of the JVM process run by isabelle build. |
|
912 |
||
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
52060
diff
changeset
|
913 |
* Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
52060
diff
changeset
|
914 |
to run Isabelle/Scala source files as standalone programs. |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
52060
diff
changeset
|
915 |
|
52439
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
916 |
* Improved "isabelle keywords" tool (for old-style ProofGeneral |
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
917 |
keyword tables): use Isabelle/Scala operations, which inspect outer |
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
918 |
syntax without requiring to build sessions first. |
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
919 |
|
53971 | 920 |
* Sessions may be organized via 'chapter' specifications in the ROOT |
921 |
file, which determines a two-level hierarchy of browser info. The old |
|
922 |
tree-like organization via implicit sub-session relation (with its |
|
923 |
tendency towards erratic fluctuation of URLs) has been discontinued. |
|
924 |
The default chapter is called "Unsorted". Potential INCOMPATIBILITY |
|
925 |
for HTML presentation of theories. |
|
926 |
||
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
927 |
|
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
928 |
|
50993 | 929 |
New in Isabelle2013 (February 2013) |
930 |
----------------------------------- |
|
47887 | 931 |
|
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
932 |
*** General *** |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
933 |
|
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
934 |
* Theorem status about oracles and unfinished/failed future proofs is |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
935 |
no longer printed by default, since it is incompatible with |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
936 |
incremental / parallel checking of the persistent document model. ML |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
937 |
function Thm.peek_status may be used to inspect a snapshot of the |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
938 |
ongoing evaluation process. Note that in batch mode --- notably |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
939 |
isabelle build --- the system ensures that future proofs of all |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
940 |
accessible theorems in the theory context are finished (as before). |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
941 |
|
49699 | 942 |
* Configuration option show_markup controls direct inlining of markup |
943 |
into the printed representation of formal entities --- notably type |
|
944 |
and sort constraints. This enables Prover IDE users to retrieve that |
|
945 |
information via tooltips in the output window, for example. |
|
946 |
||
48890
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48844
diff
changeset
|
947 |
* Command 'ML_file' evaluates ML text from a file directly within the |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48844
diff
changeset
|
948 |
theory, without any predeclaration via 'uses' in the theory header. |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48844
diff
changeset
|
949 |
|
49243 | 950 |
* Old command 'use' command and corresponding keyword 'uses' in the |
951 |
theory header are legacy features and will be discontinued soon. |
|
952 |
Tools that load their additional source files may imitate the |
|
953 |
'ML_file' implementation, such that the system can take care of |
|
954 |
dependencies properly. |
|
955 |
||
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
956 |
* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
957 |
is called fastforce / fast_force_tac already since Isabelle2011-1. |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
958 |
|
50110 | 959 |
* Updated and extended "isar-ref" and "implementation" manual, reduced |
960 |
remaining material in old "ref" manual. |
|
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
961 |
|
51050 | 962 |
* Improved support for auxiliary contexts that indicate block structure |
963 |
for specifications. Nesting of "context fixes ... context assumes ..." |
|
49841 | 964 |
and "class ... context ...". |
965 |
||
50772
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
966 |
* Attribute "consumes" allows a negative value as well, which is |
50778 | 967 |
interpreted relatively to the total number of premises of the rule in |
50772
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
968 |
the target context. This form of declaration is stable when exported |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
969 |
from a nested 'context' with additional assumptions. It is the |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
970 |
preferred form for definitional packages, notably cases/rules produced |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
971 |
in HOL/inductive and HOL/function. |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
972 |
|
49869
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
973 |
* More informative error messages for Isar proof commands involving |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
974 |
lazy enumerations (method applications etc.). |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
975 |
|
50213 | 976 |
* Refined 'help' command to retrieve outer syntax commands according |
977 |
to name patterns (with clickable results). |
|
978 |
||
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
979 |
|
49968 | 980 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
981 |
||
982 |
* Parallel terminal proofs ('by') are enabled by default, likewise |
|
983 |
proofs that are built into packages like 'datatype', 'function'. This |
|
984 |
allows to "run ahead" checking the theory specifications on the |
|
985 |
surface, while the prover is still crunching on internal |
|
986 |
justifications. Unfinished / cancelled proofs are restarted as |
|
987 |
required to complete full proof checking eventually. |
|
988 |
||
989 |
* Improved output panel with tooltips, hyperlinks etc. based on the |
|
990 |
same Rich_Text_Area as regular Isabelle/jEdit buffers. Activation of |
|
991 |
tooltips leads to some window that supports the same recursively, |
|
992 |
which can lead to stacks of tooltips as the semantic document content |
|
993 |
is explored. ESCAPE closes the whole stack, individual windows may be |
|
994 |
closed separately, or detached to become independent jEdit dockables. |
|
995 |
||
50717 | 996 |
* Improved support for commands that produce graph output: the text |
997 |
message contains a clickable area to open a new instance of the graph |
|
998 |
browser on demand. |
|
999 |
||
49968 | 1000 |
* More robust incremental parsing of outer syntax (partial comments, |
1001 |
malformed symbols). Changing the balance of open/close quotes and |
|
1002 |
comment delimiters works more conveniently with unfinished situations |
|
1003 |
that frequently occur in user interaction. |
|
1004 |
||
1005 |
* More efficient painting and improved reactivity when editing large |
|
1006 |
files. More scalable management of formal document content. |
|
1007 |
||
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50455
diff
changeset
|
1008 |
* Smarter handling of tracing messages: prover process pauses after |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50455
diff
changeset
|
1009 |
certain number of messages per command transaction, with some user |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50455
diff
changeset
|
1010 |
dialog to stop or continue. This avoids swamping the front-end with |
50119
5c370a036de7
more generous tracing_limit, with explicit system option;
wenzelm
parents:
50118
diff
changeset
|
1011 |
potentially infinite message streams. |
49968 | 1012 |
|
1013 |
* More plugin options and preferences, based on Isabelle/Scala. The |
|
1014 |
jEdit plugin option panel provides access to some Isabelle/Scala |
|
1015 |
options, including tuning parameters for editor reactivity and color |
|
1016 |
schemes. |
|
1017 |
||
50184 | 1018 |
* Dockable window "Symbols" provides some editing support for Isabelle |
1019 |
symbols. |
|
1020 |
||
51082 | 1021 |
* Dockable window "Monitor" shows ML runtime statistics. Note that |
1022 |
continuous display of the chart slows down the system. |
|
50701 | 1023 |
|
50183 | 1024 |
* Improved editing support for control styles: subscript, superscript, |
1025 |
bold, reset of style -- operating on single symbols or text |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
1026 |
selections. Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT. |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
1027 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
1028 |
* Actions isabelle.increase-font-size and isabelle.decrease-font-size |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
1029 |
adjust the main text area font size, and its derivatives for output, |
50836 | 1030 |
tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS, which often |
1031 |
need to be adapted to local keyboard layouts. |
|
50183 | 1032 |
|
50730 | 1033 |
* More reactive completion popup by default: use \t (TAB) instead of |
1034 |
\n (NEWLINE) to minimize intrusion into regular flow of editing. See |
|
1035 |
also "Plugin Options / SideKick / General / Code Completion Options". |
|
1036 |
||
50406
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
1037 |
* Implicit check and build dialog of the specified logic session |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
1038 |
image. For example, HOL, HOLCF, HOL-Nominal can be produced on |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
1039 |
demand, without bundling big platform-dependent heap images in the |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
1040 |
Isabelle distribution. |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
1041 |
|
49968 | 1042 |
* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates |
1043 |
from Oracle provide better multi-platform experience. This version is |
|
1044 |
now bundled exclusively with Isabelle. |
|
1045 |
||
1046 |
||
48205 | 1047 |
*** Pure *** |
1048 |
||
48431
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
48428
diff
changeset
|
1049 |
* Code generation for Haskell: restrict unqualified imports from |
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
48428
diff
changeset
|
1050 |
Haskell Prelude to a small set of fundamental operations. |
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
48428
diff
changeset
|
1051 |
|
50646 | 1052 |
* Command 'export_code': relative file names are interpreted |
1053 |
relatively to master directory of current theory rather than the |
|
1054 |
rather arbitrary current working directory. INCOMPATIBILITY. |
|
48371 | 1055 |
|
48205 | 1056 |
* Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, |
1057 |
use regular rule composition via "OF" / "THEN", or explicit proof |
|
1058 |
structure instead. Note that Isabelle/ML provides a variety of |
|
1059 |
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |
|
1060 |
with some care where this is really required. |
|
1061 |
||
48792 | 1062 |
* Command 'typ' supports an additional variant with explicit sort |
1063 |
constraint, to infer and check the most general type conforming to a |
|
51063 | 1064 |
given sort. Example (in HOL): |
48792 | 1065 |
|
1066 |
typ "_ * _ * bool * unit" :: finite |
|
1067 |
||
50716 | 1068 |
* Command 'locale_deps' visualizes all locales and their relations as |
1069 |
a Hasse diagram. |
|
1070 |
||
48205 | 1071 |
|
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
1072 |
*** HOL *** |
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
1073 |
|
50646 | 1074 |
* Sledgehammer: |
1075 |
||
1076 |
- Added MaSh relevance filter based on machine-learning; see the |
|
1077 |
Sledgehammer manual for details. |
|
1078 |
- Polished Isar proofs generated with "isar_proofs" option. |
|
1079 |
- Rationalized type encodings ("type_enc" option). |
|
50720 | 1080 |
- Renamed "kill_provers" subcommand to "kill_all". |
50646 | 1081 |
- Renamed options: |
1082 |
isar_proof ~> isar_proofs |
|
1083 |
isar_shrink_factor ~> isar_shrink |
|
1084 |
max_relevant ~> max_facts |
|
1085 |
relevance_thresholds ~> fact_thresholds |
|
1086 |
||
1087 |
* Quickcheck: added an optimisation for equality premises. It is |
|
1088 |
switched on by default, and can be switched off by setting the |
|
1089 |
configuration quickcheck_optimise_equality to false. |
|
1090 |
||
50878 | 1091 |
* Quotient: only one quotient can be defined by quotient_type |
1092 |
INCOMPATIBILITY. |
|
1093 |
||
1094 |
* Lifting: |
|
1095 |
- generation of an abstraction function equation in lift_definition |
|
1096 |
- quot_del attribute |
|
1097 |
- renamed no_abs_code -> no_code (INCOMPATIBILITY.) |
|
1098 |
||
50646 | 1099 |
* Simproc "finite_Collect" rewrites set comprehensions into pointfree |
1100 |
expressions. |
|
1101 |
||
1102 |
* Preprocessing of the code generator rewrites set comprehensions into |
|
1103 |
pointfree expressions. |
|
1104 |
||
1105 |
* The SMT solver Z3 has now by default a restricted set of directly |
|
1106 |
supported features. For the full set of features (div/mod, nonlinear |
|
1107 |
arithmetic, datatypes/records) with potential proof reconstruction |
|
1108 |
failures, enable the configuration option "z3_with_extensions". Minor |
|
1109 |
INCOMPATIBILITY. |
|
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49918
diff
changeset
|
1110 |
|
49836
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
1111 |
* Simplified 'typedef' specifications: historical options for implicit |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
1112 |
set definition and alternative name have been discontinued. The |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
1113 |
former behavior of "typedef (open) t = A" is now the default, but |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
1114 |
written just "typedef t = A". INCOMPATIBILITY, need to adapt theories |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
1115 |
accordingly. |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
1116 |
|
50646 | 1117 |
* Removed constant "chars"; prefer "Enum.enum" on type "char" |
1118 |
directly. INCOMPATIBILITY. |
|
1119 |
||
1120 |
* Moved operation product, sublists and n_lists from theory Enum to |
|
1121 |
List. INCOMPATIBILITY. |
|
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49770
diff
changeset
|
1122 |
|
49739 | 1123 |
* Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. |
1124 |
||
49738 | 1125 |
* Class "comm_monoid_diff" formalises properties of bounded |
49388 | 1126 |
subtraction, with natural numbers and multisets as typical instances. |
1127 |
||
50646 | 1128 |
* Added combinator "Option.these" with type "'a option set => 'a set". |
1129 |
||
1130 |
* Theory "Transitive_Closure": renamed lemmas |
|
1131 |
||
1132 |
reflcl_tranclp -> reflclp_tranclp |
|
1133 |
rtranclp_reflcl -> rtranclp_reflclp |
|
1134 |
||
1135 |
INCOMPATIBILITY. |
|
1136 |
||
1137 |
* Theory "Rings": renamed lemmas (in class semiring) |
|
1138 |
||
1139 |
left_distrib ~> distrib_right |
|
1140 |
right_distrib ~> distrib_left |
|
1141 |
||
1142 |
INCOMPATIBILITY. |
|
1143 |
||
1144 |
* Generalized the definition of limits: |
|
1145 |
||
1146 |
- Introduced the predicate filterlim (LIM x F. f x :> G) which |
|
1147 |
expresses that when the input values x converge to F then the |
|
1148 |
output f x converges to G. |
|
1149 |
||
1150 |
- Added filters for convergence to positive (at_top) and negative |
|
1151 |
infinity (at_bot). |
|
1152 |
||
1153 |
- Moved infinity in the norm (at_infinity) from |
|
1154 |
Multivariate_Analysis to Complex_Main. |
|
1155 |
||
1156 |
- Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> |
|
1157 |
at_top". |
|
1158 |
||
1159 |
INCOMPATIBILITY. |
|
1160 |
||
1161 |
* Theory "Library/Option_ord" provides instantiation of option type to |
|
1162 |
lattice type classes. |
|
1163 |
||
1164 |
* Theory "Library/Multiset": renamed |
|
1165 |
||
1166 |
constant fold_mset ~> Multiset.fold |
|
1167 |
fact fold_mset_commute ~> fold_mset_comm |
|
1168 |
||
1169 |
INCOMPATIBILITY. |
|
1170 |
||
1171 |
* Renamed theory Library/List_Prefix to Library/Sublist, with related |
|
1172 |
changes as follows. |
|
1173 |
||
1174 |
- Renamed constants (and related lemmas) |
|
49145 | 1175 |
|
1176 |
prefix ~> prefixeq |
|
1177 |
strict_prefix ~> prefix |
|
1178 |
||
50646 | 1179 |
- Replaced constant "postfix" by "suffixeq" with swapped argument |
1180 |
order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped |
|
1181 |
old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead. |
|
1182 |
Renamed lemmas accordingly. |
|
1183 |
||
1184 |
- Added constant "list_hembeq" for homeomorphic embedding on |
|
1185 |
lists. Added abbreviation "sublisteq" for special case |
|
1186 |
"list_hembeq (op =)". |
|
1187 |
||
1188 |
- Theory Library/Sublist no longer provides "order" and "bot" type |
|
1189 |
class instances for the prefix order (merely corresponding locale |
|
1190 |
interpretations). The type class instances are now in theory |
|
1191 |
Library/Prefix_Order. |
|
1192 |
||
1193 |
- The sublist relation of theory Library/Sublist_Order is now based |
|
1194 |
on "Sublist.sublisteq". Renamed lemmas accordingly: |
|
50516 | 1195 |
|
1196 |
le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff |
|
1197 |
le_list_append_mono ~> Sublist.list_hembeq_append_mono |
|
1198 |
le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2 |
|
1199 |
le_list_Cons_EX ~> Sublist.list_hembeq_ConsD |
|
1200 |
le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2' |
|
1201 |
le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq |
|
1202 |
le_list_drop_Cons ~> Sublist.sublisteq_Cons' |
|
1203 |
le_list_drop_many ~> Sublist.sublisteq_drop_many |
|
1204 |
le_list_filter_left ~> Sublist.sublisteq_filter_left |
|
1205 |
le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many |
|
1206 |
le_list_rev_take_iff ~> Sublist.sublisteq_append |
|
1207 |
le_list_same_length ~> Sublist.sublisteq_same_length |
|
1208 |
le_list_take_many_iff ~> Sublist.sublisteq_append' |
|
49145 | 1209 |
less_eq_list.drop ~> less_eq_list_drop |
1210 |
less_eq_list.induct ~> less_eq_list_induct |
|
50516 | 1211 |
not_le_list_length ~> Sublist.not_sublisteq_length |
49145 | 1212 |
|
50646 | 1213 |
INCOMPATIBILITY. |
1214 |
||
1215 |
* New theory Library/Countable_Set. |
|
1216 |
||
1217 |
* Theory Library/Debug and Library/Parallel provide debugging and |
|
1218 |
parallel execution for code generated towards Isabelle/ML. |
|
1219 |
||
1220 |
* Theory Library/FuncSet: Extended support for Pi and extensional and |
|
1221 |
introduce the extensional dependent function space "PiE". Replaced |
|
1222 |
extensional_funcset by an abbreviation, and renamed lemmas from |
|
1223 |
extensional_funcset to PiE as follows: |
|
1224 |
||
1225 |
extensional_empty ~> PiE_empty |
|
1226 |
extensional_funcset_empty_domain ~> PiE_empty_domain |
|
1227 |
extensional_funcset_empty_range ~> PiE_empty_range |
|
1228 |
extensional_funcset_arb ~> PiE_arb |
|
1229 |
extensional_funcset_mem ~> PiE_mem |
|
1230 |
extensional_funcset_extend_domainI ~> PiE_fun_upd |
|
1231 |
extensional_funcset_restrict_domain ~> fun_upd_in_PiE |
|
1232 |
extensional_funcset_extend_domain_eq ~> PiE_insert_eq |
|
1233 |
card_extensional_funcset ~> card_PiE |
|
1234 |
finite_extensional_funcset ~> finite_PiE |
|
1235 |
||
1236 |
INCOMPATIBILITY. |
|
1237 |
||
1238 |
* Theory Library/FinFun: theory of almost everywhere constant |
|
1239 |
functions (supersedes the AFP entry "Code Generation for Functions as |
|
1240 |
Data"). |
|
1241 |
||
1242 |
* Theory Library/Phantom: generic phantom type to make a type |
|
1243 |
parameter appear in a constant's type. This alternative to adding |
|
1244 |
TYPE('a) as another parameter avoids unnecessary closures in generated |
|
1245 |
code. |
|
1246 |
||
1247 |
* Theory Library/RBT_Impl: efficient construction of red-black trees |
|
1248 |
from sorted associative lists. Merging two trees with rbt_union may |
|
1249 |
return a structurally different tree than before. Potential |
|
1250 |
INCOMPATIBILITY. |
|
1251 |
||
1252 |
* Theory Library/IArray: immutable arrays with code generation. |
|
1253 |
||
1254 |
* Theory Library/Finite_Lattice: theory of finite lattices. |
|
1255 |
||
1256 |
* HOL/Multivariate_Analysis: replaced |
|
1257 |
||
1258 |
"basis :: 'a::euclidean_space => nat => real" |
|
1259 |
"\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space" |
|
1260 |
||
1261 |
on euclidean spaces by using the inner product "_ \<bullet> _" with |
|
1262 |
vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by |
|
1263 |
"SUM i : Basis. f i * r i". |
|
1264 |
||
1265 |
With this change the following constants are also changed or removed: |
|
1266 |
||
1267 |
DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation) |
|
1268 |
a $$ i ~> inner a i (where i : Basis) |
|
1269 |
cart_base i removed |
|
1270 |
\<pi>, \<pi>' removed |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
1271 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
1272 |
Theorems about these constants where removed. |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
1273 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
1274 |
Renamed lemmas: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
1275 |
|
50646 | 1276 |
component_le_norm ~> Basis_le_norm |
1277 |
euclidean_eq ~> euclidean_eq_iff |
|
1278 |
differential_zero_maxmin_component ~> differential_zero_maxmin_cart |
|
1279 |
euclidean_simps ~> inner_simps |
|
1280 |
independent_basis ~> independent_Basis |
|
1281 |
span_basis ~> span_Basis |
|
1282 |
in_span_basis ~> in_span_Basis |
|
1283 |
norm_bound_component_le ~> norm_boound_Basis_le |
|
1284 |
norm_bound_component_lt ~> norm_boound_Basis_lt |
|
1285 |
component_le_infnorm ~> Basis_le_infnorm |
|
1286 |
||
1287 |
INCOMPATIBILITY. |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
1288 |
|
50141 | 1289 |
* HOL/Probability: |
50646 | 1290 |
|
1291 |
- Added simproc "measurable" to automatically prove measurability. |
|
1292 |
||
1293 |
- Added induction rules for sigma sets with disjoint union |
|
1294 |
(sigma_sets_induct_disjoint) and for Borel-measurable functions |
|
1295 |
(borel_measurable_induct). |
|
1296 |
||
1297 |
- Added the Daniell-Kolmogorov theorem (the existence the limit of a |
|
1298 |
projective family). |
|
1299 |
||
1300 |
* HOL/Cardinals: Theories of ordinals and cardinals (supersedes the |
|
1301 |
AFP entry "Ordinals_and_Cardinals"). |
|
1302 |
||
1303 |
* HOL/BNF: New (co)datatype package based on bounded natural functors |
|
1304 |
with support for mixed, nested recursion and interesting non-free |
|
1305 |
datatypes. |
|
48094 | 1306 |
|
50991 | 1307 |
* HOL/Finite_Set and Relation: added new set and relation operations |
50878 | 1308 |
expressed by Finite_Set.fold. |
1309 |
||
1310 |
* New theory HOL/Library/RBT_Set: implementation of sets by red-black |
|
1311 |
trees for the code generator. |
|
1312 |
||
1313 |
* HOL/Library/RBT and HOL/Library/Mapping have been converted to |
|
1314 |
Lifting/Transfer. |
|
1315 |
possible INCOMPATIBILITY. |
|
1316 |
||
1317 |
* HOL/Set: renamed Set.project -> Set.filter |
|
1318 |
INCOMPATIBILITY. |
|
1319 |
||
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
1320 |
|
48206 | 1321 |
*** Document preparation *** |
1322 |
||
50646 | 1323 |
* Dropped legacy antiquotations "term_style" and "thm_style", since |
1324 |
styles may be given as arguments to "term" and "thm" already. |
|
1325 |
Discontinued legacy styles "prem1" .. "prem19". |
|
1326 |
||
1327 |
* Default LaTeX rendering for \<euro> is now based on eurosym package, |
|
1328 |
instead of slightly exotic babel/greek. |
|
48206 | 1329 |
|
48616
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
1330 |
* Document variant NAME may use different LaTeX entry point |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
1331 |
document/root_NAME.tex if that file exists, instead of the common |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
1332 |
document/root.tex. |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
1333 |
|
48657
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
1334 |
* Simplified custom document/build script, instead of old-style |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
1335 |
document/IsaMakefile. Minor INCOMPATIBILITY. |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
1336 |
|
48206 | 1337 |
|
48992 | 1338 |
*** ML *** |
1339 |
||
50646 | 1340 |
* The default limit for maximum number of worker threads is now 8, |
1341 |
instead of 4, in correspondence to capabilities of contemporary |
|
1342 |
hardware and Poly/ML runtime system. |
|
1343 |
||
49869
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
1344 |
* Type Seq.results and related operations support embedded error |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
1345 |
messages within lazy enumerations, and thus allow to provide |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
1346 |
informative errors in the absence of any usable results. |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
1347 |
|
48992 | 1348 |
* Renamed Position.str_of to Position.here to emphasize that this is a |
1349 |
formal device to inline positions into message text, but not |
|
1350 |
necessarily printing visible text. |
|
1351 |
||
1352 |
||
48206 | 1353 |
*** System *** |
1354 |
||
48585
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
1355 |
* Advanced support for Isabelle sessions and build management, see |
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
1356 |
"system" manual for the chapter of that name, especially the "isabelle |
51056 | 1357 |
build" tool and its examples. The "isabelle mkroot" tool prepares |
1358 |
session root directories for use with "isabelle build", similar to |
|
1359 |
former "isabelle mkdir" for "isabelle usedir". Note that this affects |
|
1360 |
document preparation as well. INCOMPATIBILITY, isabelle usedir / |
|
48736 | 1361 |
mkdir / make are rendered obsolete. |
1362 |
||
51056 | 1363 |
* Discontinued obsolete Isabelle/build script, it is superseded by the |
1364 |
regular isabelle build tool. For example: |
|
1365 |
||
1366 |
isabelle build -s -b HOL |
|
1367 |
||
48736 | 1368 |
* Discontinued obsolete "isabelle makeall". |
48585
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
1369 |
|
48722
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
1370 |
* Discontinued obsolete IsaMakefile and ROOT.ML files from the |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
1371 |
Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
1372 |
provides some traditional targets that invoke "isabelle build". Note |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
1373 |
that this is inefficient! Applications of Isabelle/HOL involving |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
1374 |
"isabelle make" should be upgraded to use "isabelle build" directly. |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
1375 |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
1376 |
* The "isabelle options" tool prints Isabelle system options, as |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
1377 |
required for "isabelle build", for example. |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
1378 |
|
50646 | 1379 |
* The "isabelle logo" tool produces EPS and PDF format simultaneously. |
1380 |
Minor INCOMPATIBILITY in command-line options. |
|
1381 |
||
1382 |
* The "isabelle install" tool has now a simpler command-line. Minor |
|
1383 |
INCOMPATIBILITY. |
|
1384 |
||
48844 | 1385 |
* The "isabelle components" tool helps to resolve add-on components |
1386 |
that are not bundled, or referenced from a bare-bones repository |
|
1387 |
version of Isabelle. |
|
1388 |
||
50646 | 1389 |
* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general |
1390 |
platform family: "linux", "macos", "windows". |
|
1391 |
||
1392 |
* The ML system is configured as regular component, and no longer |
|
1393 |
picked up from some surrounding directory. Potential INCOMPATIBILITY |
|
1394 |
for home-made settings. |
|
50132 | 1395 |
|
50701 | 1396 |
* Improved ML runtime statistics (heap, threads, future tasks etc.). |
1397 |
||
48206 | 1398 |
* Discontinued support for Poly/ML 5.2.1, which was the last version |
1399 |
without exception positions and advanced ML compiler/toplevel |
|
1400 |
configuration. |
|
1401 |
||
48574 | 1402 |
* Discontinued special treatment of Proof General -- no longer guess |
1403 |
PROOFGENERAL_HOME based on accidental file-system layout. Minor |
|
1404 |
INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS |
|
1405 |
settings manually, or use a Proof General version that has been |
|
1406 |
bundled as Isabelle component. |
|
48206 | 1407 |
|
50182 | 1408 |
|
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
1409 |
|
47462 | 1410 |
New in Isabelle2012 (May 2012) |
1411 |
------------------------------ |
|
45109 | 1412 |
|
45593 | 1413 |
*** General *** |
1414 |
||
45614 | 1415 |
* Prover IDE (PIDE) improvements: |
1416 |
||
47585 | 1417 |
- more robust Sledgehammer integration (as before the sledgehammer |
47806 | 1418 |
command-line needs to be typed into the source buffer) |
45614 | 1419 |
- markup for bound variables |
47806 |