author | blanchet |
Mon, 18 Aug 2014 17:19:58 +0200 | |
changeset 57983 | 6edc3529bb4e |
parent 57946 | 6a26aa5fa65e |
child 57990 | 90d941a477bd |
permissions | -rw-r--r-- |
57491 | 1 |
Isabelle NEWS -- history of user-relevant changes |
2 |
================================================= |
|
2553 | 3 |
|
57695 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
6 |
||
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
7 |
*** General *** |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
8 |
|
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
9 |
* Commands 'method_setup' and 'attribute_setup' now work within a |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
10 |
local theory context. |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
11 |
|
57946
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
12 |
* Command 'named_theorems' declares a dynamic fact within the context, |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
13 |
together with an attribute to maintain the content incrementally. |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
14 |
This supersedes functor Named_Thms, but with a subtle change of |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
15 |
semantics due to external visual order vs. internal reverse order. |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
16 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
17 |
|
57737 | 18 |
*** HOL *** |
19 |
||
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
20 |
* New (co)datatype package: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
21 |
- Renamed theorems: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
22 |
disc_corec ~> corec_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
23 |
disc_corec_iff ~> corec_disc_iff |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
24 |
disc_exclude ~> distinct_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
25 |
disc_exhaust ~> exhaust_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
26 |
disc_map_iff ~> map_disc_iff |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
27 |
sel_corec ~> corec_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
28 |
sel_exhaust ~> exhaust_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
29 |
sel_map ~> map_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
30 |
sel_set ~> set_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
31 |
sel_split ~> split_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
32 |
sel_split_asm ~> split_sel_asm |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
33 |
strong_coinduct ~> coinduct_strong |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
34 |
weak_case_cong ~> case_cong_weak |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
35 |
INCOMPATIBILITY. |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
36 |
|
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
37 |
* Old datatype package: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
38 |
- Renamed theorems: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
39 |
weak_case_cong ~> case_cong_weak |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
40 |
INCOMPATIBILITY. |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
41 |
|
57737 | 42 |
* Sledgehammer: |
43 |
- Minimization is now always enabled by default. |
|
44 |
Removed subcommand: |
|
45 |
min |
|
46 |
||
57695 | 47 |
|
48 |
||
57452 | 49 |
New in Isabelle2014 (August 2014) |
50 |
--------------------------------- |
|
54055 | 51 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
52 |
*** General *** |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
53 |
|
57452 | 54 |
* Support for official Standard ML within the Isabelle context. |
55 |
Command 'SML_file' reads and evaluates the given Standard ML file. |
|
56 |
Toplevel bindings are stored within the theory context; the initial |
|
57 |
environment is restricted to the Standard ML implementation of |
|
58 |
Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import' |
|
59 |
and 'SML_export' allow to exchange toplevel bindings between the two |
|
60 |
separate environments. See also ~~/src/Tools/SML/Examples.thy for |
|
61 |
some examples. |
|
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56450
diff
changeset
|
62 |
|
57504 | 63 |
* Standard tactics and proof methods such as "clarsimp", "auto" and |
64 |
"safe" now preserve equality hypotheses "x = expr" where x is a free |
|
65 |
variable. Locale assumptions and chained facts containing "x" |
|
66 |
continue to be useful. The new method "hypsubst_thin" and the |
|
67 |
configuration option "hypsubst_thin" (within the attribute name space) |
|
68 |
restore the previous behavior. INCOMPATIBILITY, especially where |
|
69 |
induction is done after these methods or when the names of free and |
|
70 |
bound variables clash. As first approximation, old proofs may be |
|
71 |
repaired by "using [[hypsubst_thin = true]]" in the critical spot. |
|
72 |
||
56232 | 73 |
* More static checking of proof methods, which allows the system to |
74 |
form a closure over the concrete syntax. Method arguments should be |
|
75 |
processed in the original proof context as far as possible, before |
|
76 |
operating on the goal state. In any case, the standard discipline for |
|
77 |
subgoal-addressing needs to be observed: no subgoals or a subgoal |
|
78 |
number that is out of range produces an empty result sequence, not an |
|
79 |
exception. Potential INCOMPATIBILITY for non-conformant tactical |
|
80 |
proof tools. |
|
81 |
||
57452 | 82 |
* Lexical syntax (inner and outer) supports text cartouches with |
83 |
arbitrary nesting, and without escapes of quotes etc. The Prover IDE |
|
84 |
supports input via ` (backquote). |
|
85 |
||
86 |
* The outer syntax categories "text" (for formal comments and document |
|
87 |
markup commands) and "altstring" (for literal fact references) allow |
|
88 |
cartouches as well, in addition to the traditional mix of quotations. |
|
89 |
||
90 |
* Syntax of document antiquotation @{rail} now uses \<newline> instead |
|
91 |
of "\\", to avoid the optical illusion of escaped backslash within |
|
57491 | 92 |
string token. General renovation of its syntax using text cartouches. |
57452 | 93 |
Minor INCOMPATIBILITY. |
94 |
||
95 |
* Discontinued legacy_isub_isup, which was a temporary workaround for |
|
96 |
Isabelle/ML in Isabelle2013-1. The prover process no longer accepts |
|
97 |
old identifier syntax with \<^isub> or \<^isup>. Potential |
|
98 |
INCOMPATIBILITY. |
|
99 |
||
100 |
* Document antiquotation @{url} produces markup for the given URL, |
|
101 |
which results in an active hyperlink within the text. |
|
102 |
||
103 |
* Document antiquotation @{file_unchecked} is like @{file}, but does |
|
104 |
not check existence within the file-system. |
|
105 |
||
106 |
* Updated and extended manuals: codegen, datatypes, implementation, |
|
107 |
isar-ref, jedit, system. |
|
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
108 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
109 |
|
54533 | 110 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
111 |
||
57650 | 112 |
* Improved Document panel: simplified interaction where every single |
57452 | 113 |
mouse click (re)opens document via desktop environment or as jEdit |
114 |
buffer. |
|
115 |
||
116 |
* Support for Navigator plugin (with toolbar buttons), with connection |
|
117 |
to PIDE hyperlinks. |
|
118 |
||
119 |
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. |
|
120 |
Open text buffers take precedence over copies within the file-system. |
|
121 |
||
122 |
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for |
|
123 |
auxiliary ML files. |
|
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
124 |
|
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
125 |
* Improved syntactic and semantic completion mechanism, with simple |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
126 |
templates, completion language context, name-space completion, |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
127 |
file-name completion, spell-checker completion. |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
128 |
|
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
129 |
* Refined GUI popup for completion: more robust key/mouse event |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
130 |
handling and propagation to enclosing text area -- avoid loosing |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
131 |
keystrokes with slow / remote graphics displays. |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
132 |
|
57833
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset
|
133 |
* Completion popup supports both ENTER and TAB (default) to select an |
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset
|
134 |
item, depending on Isabelle options. |
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset
|
135 |
|
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
136 |
* Refined insertion of completion items wrt. jEdit text: multiple |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
137 |
selections, rectangular selections, rectangular selection as "tall |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
138 |
caret". |
56342 | 139 |
|
56580 | 140 |
* Integrated spell-checker for document text, comments etc. with |
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
141 |
completion popup and context-menu. |
56554 | 142 |
|
56879
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
143 |
* More general "Query" panel supersedes "Find" panel, with GUI access |
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
144 |
to commands 'find_theorems' and 'find_consts', as well as print |
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
145 |
operations for the context. Minor incompatibility in keyboard |
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
146 |
shortcuts etc.: replace action isabelle-find by isabelle-query. |
56761 | 147 |
|
56901 | 148 |
* Search field for all output panels ("Output", "Query", "Info" etc.) |
149 |
to highlight text via regular expression. |
|
150 |
||
54881 | 151 |
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle / |
152 |
General") allows to specify additional print modes for the prover |
|
153 |
process, without requiring old-fashioned command-line invocation of |
|
154 |
"isabelle jedit -m MODE". |
|
155 |
||
56505 | 156 |
* More support for remote files (e.g. http) using standard Java |
157 |
networking operations instead of jEdit virtual file-systems. |
|
158 |
||
57822 | 159 |
* Empty editors buffers that are no longer required (e.g.\ via theory |
160 |
imports) are automatically removed from the document model. |
|
161 |
||
57869 | 162 |
* Improved monitor panel. |
163 |
||
56838 | 164 |
* Improved Console/Scala plugin: more uniform scala.Console output, |
165 |
more robust treatment of threads and interrupts. |
|
166 |
||
56939 | 167 |
* Improved management of dockable windows: clarified keyboard focus |
168 |
and window placement wrt. main editor view; optional menu item to |
|
169 |
"Detach" a copy where this makes sense. |
|
170 |
||
57452 | 171 |
* New Simplifier Trace panel provides an interactive view of the |
57594
8c095aef6769
clarified "simp_trace_new" and corresponding isar-ref section;
wenzelm
parents:
57532
diff
changeset
|
172 |
simplification process, enabled by the "simp_trace_new" attribute |
57452 | 173 |
within the context. |
174 |
||
175 |
||
55001 | 176 |
*** Pure *** |
177 |
||
57504 | 178 |
* Low-level type-class commands 'classes', 'classrel', 'arities' have |
179 |
been discontinued to avoid the danger of non-trivial axiomatization |
|
180 |
that is not immediately visible. INCOMPATIBILITY, use regular |
|
181 |
'instance' command with proof. The required OFCLASS(...) theorem |
|
182 |
might be postulated via 'axiomatization' beforehand, or the proof |
|
183 |
finished trivially if the underlying class definition is made vacuous |
|
184 |
(without any assumptions). See also Isabelle/ML operations |
|
185 |
Axclass.class_axiomatization, Axclass.classrel_axiomatization, |
|
186 |
Axclass.arity_axiomatization. |
|
187 |
||
56245 | 188 |
* Basic constants of Pure use more conventional names and are always |
189 |
qualified. Rare INCOMPATIBILITY, but with potentially serious |
|
190 |
consequences, notably for tools in Isabelle/ML. The following |
|
191 |
renaming needs to be applied: |
|
192 |
||
193 |
== ~> Pure.eq |
|
194 |
==> ~> Pure.imp |
|
195 |
all ~> Pure.all |
|
196 |
TYPE ~> Pure.type |
|
197 |
dummy_pattern ~> Pure.dummy_pattern |
|
198 |
||
199 |
Systematic porting works by using the following theory setup on a |
|
200 |
*previous* Isabelle version to introduce the new name accesses for the |
|
201 |
old constants: |
|
202 |
||
203 |
setup {* |
|
204 |
fn thy => thy |
|
205 |
|> Sign.root_path |
|
206 |
|> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "==" |
|
207 |
|> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>" |
|
208 |
|> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all" |
|
209 |
|> Sign.restore_naming thy |
|
210 |
*} |
|
211 |
||
212 |
Thus ML antiquotations like @{const_name Pure.eq} may be used already. |
|
213 |
Later the application is moved to the current Isabelle version, and |
|
214 |
the auxiliary aliases are deleted. |
|
215 |
||
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
216 |
* 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
|
217 |
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
|
218 |
instantiated theorem. |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
219 |
|
55152 | 220 |
* Obsolete attribute "standard" has been discontinued (legacy since |
221 |
Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context |
|
222 |
where instantiations with schematic variables are intended (for |
|
223 |
declaration commands like 'lemmas' or attributes like "of"). The |
|
224 |
following temporary definition may help to port old applications: |
|
225 |
||
226 |
attribute_setup standard = |
|
227 |
"Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))" |
|
228 |
||
55001 | 229 |
* More thorough check of proof context for goal statements and |
55006 | 230 |
attributed fact expressions (concerning background theory, declared |
231 |
hyps). Potential INCOMPATIBILITY, tools need to observe standard |
|
232 |
context discipline. See also Assumption.add_assumes and the more |
|
233 |
primitive Thm.assume_hyps. |
|
55001 | 234 |
|
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
235 |
* Inner syntax token language allows regular quoted strings "..." |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
236 |
(only makes sense in practice, if outer syntax is delimited |
57452 | 237 |
differently, e.g. via cartouches). |
238 |
||
57504 | 239 |
* Command 'print_term_bindings' supersedes 'print_binds' for clarity, |
240 |
but the latter is retained some time as Proof General legacy. |
|
241 |
||
57452 | 242 |
* Code generator preprocessor: explicit control of simp tracing on a |
243 |
per-constant basis. See attribute "code_preproc". |
|
57430
020cea57eaa4
tracing facilities for the code generator preprocessor
haftmann
parents:
57423
diff
changeset
|
244 |
|
55001 | 245 |
|
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset
|
246 |
*** HOL *** |
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset
|
247 |
|
57504 | 248 |
* Code generator: enforce case of identifiers only for strict target |
249 |
language requirements. INCOMPATIBILITY. |
|
250 |
||
251 |
* Code generator: explicit proof contexts in many ML interfaces. |
|
252 |
INCOMPATIBILITY. |
|
253 |
||
254 |
* Code generator: minimize exported identifiers by default. Minor |
|
255 |
INCOMPATIBILITY. |
|
256 |
||
257 |
* Code generation for SML and OCaml: dropped arcane "no_signatures" |
|
258 |
option. Minor INCOMPATIBILITY. |
|
259 |
||
260 |
* "declare [[code abort: ...]]" replaces "code_abort ...". |
|
261 |
INCOMPATIBILITY. |
|
262 |
||
263 |
* "declare [[code drop: ...]]" drops all code equations associated |
|
264 |
with the given constants. |
|
265 |
||
266 |
* Code generations are provided for make, fields, extend and truncate |
|
267 |
operations on records. |
|
57437 | 268 |
|
57452 | 269 |
* Command and antiquotation "value" are now hardcoded against nbe and |
270 |
ML. Minor INCOMPATIBILITY. |
|
271 |
||
57504 | 272 |
* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY. |
273 |
||
274 |
* The symbol "\<newline>" may be used within char or string literals |
|
275 |
to represent (Char Nibble0 NibbleA), i.e. ASCII newline. |
|
276 |
||
277 |
* Qualified String.implode and String.explode. INCOMPATIBILITY. |
|
56923 | 278 |
|
57452 | 279 |
* Simplifier: Enhanced solver of preconditions of rewrite rules can |
280 |
now deal with conjunctions. For help with converting proofs, the old |
|
281 |
behaviour of the simplifier can be restored like this: declare/using |
|
282 |
[[simp_legacy_precond]]. This configuration option will disappear |
|
283 |
again in the future. INCOMPATIBILITY. |
|
56073
29e308b56d23
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents:
56072
diff
changeset
|
284 |
|
55139 | 285 |
* Simproc "finite_Collect" is no longer enabled by default, due to |
286 |
spurious crashes and other surprises. Potential INCOMPATIBILITY. |
|
287 |
||
57452 | 288 |
* Moved new (co)datatype package and its dependencies from session |
289 |
"HOL-BNF" to "HOL". The commands 'bnf', 'wrap_free_constructors', |
|
290 |
'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now |
|
291 |
part of theory "Main". |
|
292 |
||
55098 | 293 |
Theory renamings: |
294 |
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) |
|
295 |
Library/Wfrec.thy ~> Wfrec.thy |
|
296 |
Library/Zorn.thy ~> Zorn.thy |
|
297 |
Cardinals/Order_Relation.thy ~> Order_Relation.thy |
|
298 |
Library/Order_Union.thy ~> Cardinals/Order_Union.thy |
|
299 |
Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy |
|
300 |
Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy |
|
301 |
Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy |
|
302 |
Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy |
|
303 |
Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy |
|
304 |
BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy |
|
305 |
BNF/Basic_BNFs.thy ~> Basic_BNFs.thy |
|
306 |
BNF/BNF_Comp.thy ~> BNF_Comp.thy |
|
307 |
BNF/BNF_Def.thy ~> BNF_Def.thy |
|
308 |
BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy |
|
309 |
BNF/BNF_GFP.thy ~> BNF_GFP.thy |
|
310 |
BNF/BNF_LFP.thy ~> BNF_LFP.thy |
|
311 |
BNF/BNF_Util.thy ~> BNF_Util.thy |
|
312 |
BNF/Coinduction.thy ~> Coinduction.thy |
|
313 |
BNF/More_BNFs.thy ~> Library/More_BNFs.thy |
|
314 |
BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy |
|
315 |
BNF/Examples/* ~> BNF_Examples/* |
|
57452 | 316 |
|
55098 | 317 |
New theories: |
318 |
Wellorder_Extension.thy (split from Zorn.thy) |
|
319 |
Library/Cardinal_Notations.thy |
|
56942 | 320 |
Library/BNF_Axomatization.thy |
55098 | 321 |
BNF_Examples/Misc_Primcorec.thy |
322 |
BNF_Examples/Stream_Processor.thy |
|
57452 | 323 |
|
55519 | 324 |
Discontinued theories: |
55098 | 325 |
BNF/BNF.thy |
326 |
BNF/Equiv_Relations_More.thy |
|
57452 | 327 |
|
328 |
INCOMPATIBILITY. |
|
55098 | 329 |
|
56118
d3967fdc800a
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
blanchet
parents:
56076
diff
changeset
|
330 |
* New (co)datatype package: |
57452 | 331 |
- Command 'primcorec' is fully implemented. |
332 |
- Command 'datatype_new' generates size functions ("size_xxx" and |
|
333 |
"size") as required by 'fun'. |
|
334 |
- BNFs are integrated with the Lifting tool and new-style |
|
335 |
(co)datatypes with Transfer. |
|
336 |
- Renamed commands: |
|
55875 | 337 |
datatype_new_compat ~> datatype_compat |
338 |
primrec_new ~> primrec |
|
339 |
wrap_free_constructors ~> free_constructors |
|
340 |
INCOMPATIBILITY. |
|
57452 | 341 |
- The generated constants "xxx_case" and "xxx_rec" have been renamed |
55875 | 342 |
"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod"). |
343 |
INCOMPATIBILITY. |
|
57452 | 344 |
- The constant "xxx_(un)fold" and related theorems are no longer |
345 |
generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually |
|
346 |
using "prim(co)rec". |
|
55875 | 347 |
INCOMPATIBILITY. |
57452 | 348 |
- No discriminators are generated for nullary constructors by |
349 |
default, eliminating the need for the odd "=:" syntax. |
|
57091 | 350 |
INCOMPATIBILITY. |
57452 | 351 |
- No discriminators or selectors are generated by default by |
57094
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset
|
352 |
"datatype_new", unless custom names are specified or the new |
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset
|
353 |
"discs_sels" option is passed. |
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset
|
354 |
INCOMPATIBILITY. |
55875 | 355 |
|
55643 | 356 |
* Old datatype package: |
57452 | 357 |
- The generated theorems "xxx.cases" and "xxx.recs" have been |
358 |
renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> |
|
359 |
"sum.case"). INCOMPATIBILITY. |
|
360 |
- The generated constants "xxx_case", "xxx_rec", and "xxx_size" have |
|
361 |
been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., |
|
362 |
"prod_case" ~> "case_prod"). INCOMPATIBILITY. |
|
363 |
||
364 |
* The types "'a list" and "'a option", their set and map functions, |
|
365 |
their relators, and their selectors are now produced using the new |
|
366 |
BNF-based datatype package. |
|
367 |
||
55519 | 368 |
Renamed constants: |
369 |
Option.set ~> set_option |
|
370 |
Option.map ~> map_option |
|
55525 | 371 |
option_rel ~> rel_option |
57452 | 372 |
|
55519 | 373 |
Renamed theorems: |
55585 | 374 |
set_def ~> set_rec[abs_def] |
55519 | 375 |
map_def ~> map_rec[abs_def] |
376 |
Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") |
|
56652 | 377 |
option.recs ~> option.rec |
55524
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55519
diff
changeset
|
378 |
list_all2_def ~> list_all2_iff |
55585 | 379 |
set.simps ~> set_simps (or the slightly different "list.set") |
55519 | 380 |
map.simps ~> list.map |
381 |
hd.simps ~> list.sel(1) |
|
382 |
tl.simps ~> list.sel(2-3) |
|
383 |
the.simps ~> option.sel |
|
57452 | 384 |
|
385 |
INCOMPATIBILITY. |
|
55519 | 386 |
|
55933 | 387 |
* The following map functions and relators have been renamed: |
55939 | 388 |
sum_map ~> map_sum |
389 |
map_pair ~> map_prod |
|
55944 | 390 |
prod_rel ~> rel_prod |
55943 | 391 |
sum_rel ~> rel_sum |
55945 | 392 |
fun_rel ~> rel_fun |
55942 | 393 |
set_rel ~> rel_set |
394 |
filter_rel ~> rel_filter |
|
57452 | 395 |
fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy") |
396 |
cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy") |
|
397 |
vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy") |
|
398 |
||
399 |
INCOMPATIBILITY. |
|
400 |
||
57826 | 401 |
* Lifting and Transfer: |
402 |
- a type variable as a raw type is supported |
|
403 |
- stronger reflexivity prover |
|
404 |
- rep_eq is always generated by lift_definition |
|
57856 | 405 |
- setup for Lifting/Transfer is now automated for BNFs |
57826 | 406 |
+ holds for BNFs that do not contain a dead variable |
57856 | 407 |
+ relator_eq, relator_mono, relator_distr, relator_domain, |
57826 | 408 |
relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total, |
409 |
right_unique, right_total, left_unique, left_total are proved |
|
410 |
automatically |
|
411 |
+ definition of a predicator is generated automatically |
|
412 |
+ simplification rules for a predicator definition are proved |
|
413 |
automatically for datatypes |
|
414 |
- consolidation of the setup of Lifting/Transfer |
|
57856 | 415 |
+ property that a relator preservers reflexivity is not needed any |
57826 | 416 |
more |
417 |
Minor INCOMPATIBILITY. |
|
57856 | 418 |
+ left_total and left_unique rules are now transfer rules |
57826 | 419 |
(reflexivity_rule attribute not needed anymore) |
420 |
INCOMPATIBILITY. |
|
57856 | 421 |
+ Domainp does not have to be a separate assumption in |
57826 | 422 |
relator_domain theorems (=> more natural statement) |
423 |
INCOMPATIBILITY. |
|
424 |
- registration of code equations is more robust |
|
425 |
Potential INCOMPATIBILITY. |
|
426 |
- respectfulness proof obligation is preprocessed to a more readable |
|
427 |
form |
|
428 |
Potential INCOMPATIBILITY. |
|
429 |
- eq_onp is always unfolded in respectfulness proof obligation |
|
430 |
Potential INCOMPATIBILITY. |
|
57856 | 431 |
- unregister lifting setup for Code_Numeral.integer and |
57826 | 432 |
Code_Numeral.natural |
433 |
Potential INCOMPATIBILITY. |
|
434 |
- Lifting.invariant -> eq_onp |
|
435 |
INCOMPATIBILITY. |
|
57856 | 436 |
|
57508 | 437 |
* New internal SAT solver "cdclite" that produces models and proof |
438 |
traces. This solver replaces the internal SAT solvers "enumerate" and |
|
439 |
"dpll". Applications that explicitly used one of these two SAT |
|
440 |
solvers should use "cdclite" instead. In addition, "cdclite" is now |
|
441 |
the default SAT solver for the "sat" and "satx" proof methods and |
|
442 |
corresponding tactics; the old default can be restored using "declare |
|
443 |
[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. |
|
444 |
||
445 |
* SMT module: A new version of the SMT module, temporarily called |
|
446 |
"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g., |
|
447 |
4.3). The new proof method is called "smt2". CVC3 and CVC4 are also |
|
448 |
supported as oracles. Yices is no longer supported, because no version |
|
449 |
of the solver can handle both SMT-LIB 2 and quantifiers. |
|
450 |
||
451 |
* Activation of Z3 now works via "z3_non_commercial" system option |
|
452 |
(without requiring restart), instead of former settings variable |
|
453 |
"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu |
|
454 |
Plugin Options / Isabelle / General. |
|
455 |
||
456 |
* Sledgehammer: |
|
457 |
- Z3 can now produce Isar proofs. |
|
458 |
- MaSh overhaul: |
|
57532 | 459 |
. New SML-based learning algorithms eliminate the dependency on |
57508 | 460 |
Python and increase performance and reliability. |
461 |
. MaSh and MeSh are now used by default together with the |
|
462 |
traditional MePo (Meng-Paulson) relevance filter. To disable |
|
463 |
MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin |
|
464 |
Options / Isabelle / General to "none". |
|
465 |
- New option: |
|
466 |
smt_proofs |
|
467 |
- Renamed options: |
|
468 |
isar_compress ~> compress |
|
469 |
isar_try0 ~> try0 |
|
470 |
||
471 |
INCOMPATIBILITY. |
|
472 |
||
473 |
* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. |
|
474 |
||
475 |
* Nitpick: |
|
476 |
- Fixed soundness bug whereby mutually recursive datatypes could |
|
477 |
take infinite values. |
|
478 |
- Fixed soundness bug with low-level number functions such as |
|
479 |
"Abs_Integ" and "Rep_Integ". |
|
480 |
- Removed "std" option. |
|
481 |
- Renamed "show_datatypes" to "show_types" and "hide_datatypes" to |
|
482 |
"hide_types". |
|
483 |
||
484 |
* Metis: Removed legacy proof method 'metisFT'. Use 'metis |
|
485 |
(full_types)' instead. INCOMPATIBILITY. |
|
486 |
||
487 |
* Try0: Added 'algebra' and 'meson' to the set of proof methods. |
|
488 |
||
489 |
* Adjustion of INF and SUP operations: |
|
490 |
- Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. |
|
491 |
- Consolidated theorem names containing INFI and SUPR: have INF and |
|
492 |
SUP instead uniformly. |
|
493 |
- More aggressive normalization of expressions involving INF and Inf |
|
494 |
or SUP and Sup. |
|
495 |
- INF_image and SUP_image do not unfold composition. |
|
496 |
- Dropped facts INF_comp, SUP_comp. |
|
497 |
- Default congruence rules strong_INF_cong and strong_SUP_cong, with |
|
498 |
simplifier implication in premises. Generalize and replace former |
|
499 |
INT_cong, SUP_cong |
|
500 |
||
501 |
INCOMPATIBILITY. |
|
502 |
||
503 |
* SUP and INF generalized to conditionally_complete_lattice. |
|
504 |
||
505 |
* Swapped orientation of facts image_comp and vimage_comp: |
|
506 |
||
507 |
image_compose ~> image_comp [symmetric] |
|
508 |
image_comp ~> image_comp [symmetric] |
|
509 |
vimage_compose ~> vimage_comp [symmetric] |
|
510 |
vimage_comp ~> vimage_comp [symmetric] |
|
511 |
||
512 |
INCOMPATIBILITY. |
|
513 |
||
57504 | 514 |
* Theory reorganization: split of Big_Operators.thy into |
515 |
Groups_Big.thy and Lattices_Big.thy. |
|
55098 | 516 |
|
57418 | 517 |
* Consolidated some facts about big group operators: |
518 |
||
519 |
setsum_0' ~> setsum.neutral |
|
520 |
setsum_0 ~> setsum.neutral_const |
|
521 |
setsum_addf ~> setsum.distrib |
|
522 |
setsum_cartesian_product ~> setsum.cartesian_product |
|
523 |
setsum_cases ~> setsum.If_cases |
|
524 |
setsum_commute ~> setsum.commute |
|
525 |
setsum_cong ~> setsum.cong |
|
526 |
setsum_delta ~> setsum.delta |
|
527 |
setsum_delta' ~> setsum.delta' |
|
528 |
setsum_diff1' ~> setsum.remove |
|
529 |
setsum_empty ~> setsum.empty |
|
530 |
setsum_infinite ~> setsum.infinite |
|
531 |
setsum_insert ~> setsum.insert |
|
532 |
setsum_inter_restrict'' ~> setsum.inter_filter |
|
533 |
setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left |
|
534 |
setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right |
|
535 |
setsum_mono_zero_left ~> setsum.mono_neutral_left |
|
536 |
setsum_mono_zero_right ~> setsum.mono_neutral_right |
|
537 |
setsum_reindex ~> setsum.reindex |
|
538 |
setsum_reindex_cong ~> setsum.reindex_cong |
|
539 |
setsum_reindex_nonzero ~> setsum.reindex_nontrivial |
|
540 |
setsum_restrict_set ~> setsum.inter_restrict |
|
541 |
setsum_Plus ~> setsum.Plus |
|
542 |
setsum_setsum_restrict ~> setsum.commute_restrict |
|
543 |
setsum_Sigma ~> setsum.Sigma |
|
544 |
setsum_subset_diff ~> setsum.subset_diff |
|
545 |
setsum_Un_disjoint ~> setsum.union_disjoint |
|
546 |
setsum_UN_disjoint ~> setsum.UNION_disjoint |
|
547 |
setsum_Un_Int ~> setsum.union_inter |
|
548 |
setsum_Union_disjoint ~> setsum.Union_disjoint |
|
549 |
setsum_UNION_zero ~> setsum.Union_comp |
|
550 |
setsum_Un_zero ~> setsum.union_inter_neutral |
|
551 |
strong_setprod_cong ~> setprod.strong_cong |
|
552 |
strong_setsum_cong ~> setsum.strong_cong |
|
553 |
setprod_1' ~> setprod.neutral |
|
554 |
setprod_1 ~> setprod.neutral_const |
|
555 |
setprod_cartesian_product ~> setprod.cartesian_product |
|
556 |
setprod_cong ~> setprod.cong |
|
557 |
setprod_delta ~> setprod.delta |
|
558 |
setprod_delta' ~> setprod.delta' |
|
559 |
setprod_empty ~> setprod.empty |
|
560 |
setprod_infinite ~> setprod.infinite |
|
561 |
setprod_insert ~> setprod.insert |
|
562 |
setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left |
|
563 |
setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right |
|
564 |
setprod_mono_one_left ~> setprod.mono_neutral_left |
|
565 |
setprod_mono_one_right ~> setprod.mono_neutral_right |
|
566 |
setprod_reindex ~> setprod.reindex |
|
567 |
setprod_reindex_cong ~> setprod.reindex_cong |
|
568 |
setprod_reindex_nonzero ~> setprod.reindex_nontrivial |
|
569 |
setprod_Sigma ~> setprod.Sigma |
|
570 |
setprod_subset_diff ~> setprod.subset_diff |
|
571 |
setprod_timesf ~> setprod.distrib |
|
572 |
setprod_Un2 ~> setprod.union_diff2 |
|
573 |
setprod_Un_disjoint ~> setprod.union_disjoint |
|
574 |
setprod_UN_disjoint ~> setprod.UNION_disjoint |
|
575 |
setprod_Un_Int ~> setprod.union_inter |
|
576 |
setprod_Union_disjoint ~> setprod.Union_disjoint |
|
577 |
setprod_Un_one ~> setprod.union_inter_neutral |
|
578 |
||
579 |
Dropped setsum_cong2 (simple variant of setsum.cong). |
|
580 |
Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict) |
|
581 |
Dropped setsum_reindex_id, setprod_reindex_id |
|
582 |
(simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]). |
|
583 |
||
57452 | 584 |
INCOMPATIBILITY. |
585 |
||
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
586 |
* Abolished slightly odd global lattice interpretation for min/max. |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
587 |
|
57452 | 588 |
Fact consolidations: |
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
589 |
min_max.inf_assoc ~> min.assoc |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
590 |
min_max.inf_commute ~> min.commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
591 |
min_max.inf_left_commute ~> min.left_commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
592 |
min_max.inf_idem ~> min.idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
593 |
min_max.inf_left_idem ~> min.left_idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
594 |
min_max.inf_right_idem ~> min.right_idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
595 |
min_max.sup_assoc ~> max.assoc |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
596 |
min_max.sup_commute ~> max.commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
597 |
min_max.sup_left_commute ~> max.left_commute |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
598 |
min_max.sup_idem ~> max.idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
599 |
min_max.sup_left_idem ~> max.left_idem |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
600 |
min_max.sup_inf_distrib1 ~> max_min_distrib2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
601 |
min_max.sup_inf_distrib2 ~> max_min_distrib1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
602 |
min_max.inf_sup_distrib1 ~> min_max_distrib2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
603 |
min_max.inf_sup_distrib2 ~> min_max_distrib1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
604 |
min_max.distrib ~> min_max_distribs |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
605 |
min_max.inf_absorb1 ~> min.absorb1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
606 |
min_max.inf_absorb2 ~> min.absorb2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
607 |
min_max.sup_absorb1 ~> max.absorb1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
608 |
min_max.sup_absorb2 ~> max.absorb2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
609 |
min_max.le_iff_inf ~> min.absorb_iff1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
610 |
min_max.le_iff_sup ~> max.absorb_iff2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
611 |
min_max.inf_le1 ~> min.cobounded1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
612 |
min_max.inf_le2 ~> min.cobounded2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
613 |
le_maxI1, min_max.sup_ge1 ~> max.cobounded1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
614 |
le_maxI2, min_max.sup_ge2 ~> max.cobounded2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
615 |
min_max.le_infI1 ~> min.coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
616 |
min_max.le_infI2 ~> min.coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
617 |
min_max.le_supI1 ~> max.coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
618 |
min_max.le_supI2 ~> max.coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
619 |
min_max.less_infI1 ~> min.strict_coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
620 |
min_max.less_infI2 ~> min.strict_coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
621 |
min_max.less_supI1 ~> max.strict_coboundedI1 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
622 |
min_max.less_supI2 ~> max.strict_coboundedI2 |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
623 |
min_max.inf_mono ~> min.mono |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
624 |
min_max.sup_mono ~> max.mono |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
625 |
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
|
626 |
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
|
627 |
min_max.le_inf_iff ~> min.bounded_iff |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
628 |
min_max.le_sup_iff ~> max.bounded_iff |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
629 |
|
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
630 |
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
|
631 |
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
|
632 |
max.left_commute, max.left_idem directly. |
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
633 |
|
57452 | 634 |
For min_max.inf_sup_ord, prefer (one of) min.cobounded1, |
635 |
min.cobounded2, max.cobounded1m max.cobounded2 directly. |
|
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
636 |
|
56807 | 637 |
For min_ac or max_ac, prefer more general collection ac_simps. |
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
638 |
|
57253 | 639 |
INCOMPATBILITY. |
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset
|
640 |
|
57452 | 641 |
* Theorem disambiguation Inf_le_Sup (on finite sets) ~> |
642 |
Inf_fin_le_Sup_fin. INCOMPATIBILITY. |
|
54745 | 643 |
|
54295 | 644 |
* Qualified constant names Wellfounded.acc, Wellfounded.accp. |
645 |
INCOMPATIBILITY. |
|
646 |
||
54228 | 647 |
* Fact generalization and consolidation: |
648 |
neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 |
|
57452 | 649 |
|
650 |
INCOMPATIBILITY. |
|
651 |
||
652 |
* Purely algebraic definition of even. Fact generalization and |
|
653 |
consolidation: |
|
54228 | 654 |
nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd |
655 |
even_zero_(nat|int) ~> even_zero |
|
57452 | 656 |
|
54228 | 657 |
INCOMPATIBILITY. |
54055 | 658 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
659 |
* Abolished neg_numeral. |
57452 | 660 |
- Canonical representation for minus one is "- 1". |
661 |
- Canonical representation for other negative numbers is "- (numeral _)". |
|
662 |
- When devising rule sets for number calculation, consider the |
|
54587 | 663 |
following canonical cases: 0, 1, numeral _, - 1, - numeral _. |
57452 | 664 |
- 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
|
665 |
like "numeral One", "- numeral One", "- 0" and even "- ... - _". |
57452 | 666 |
- Syntax for negative numerals is mere input syntax. |
667 |
||
56964 | 668 |
INCOMPATIBILITY. |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54449
diff
changeset
|
669 |
|
57517 | 670 |
* Reduced name variants for rules on associativity and commutativity: |
671 |
||
672 |
add_assoc ~> add.assoc |
|
673 |
add_commute ~> add.commute |
|
674 |
add_left_commute ~> add.left_commute |
|
675 |
mult_assoc ~> mult.assoc |
|
676 |
mult_commute ~> mult.commute |
|
677 |
mult_left_commute ~> mult.left_commute |
|
678 |
nat_add_assoc ~> add.assoc |
|
679 |
nat_add_commute ~> add.commute |
|
680 |
nat_add_left_commute ~> add.left_commute |
|
681 |
nat_mult_assoc ~> mult.assoc |
|
682 |
nat_mult_commute ~> mult.commute |
|
683 |
eq_assoc ~> iff_assoc |
|
684 |
eq_left_commute ~> iff_left_commute |
|
685 |
||
686 |
INCOMPATIBILITY. |
|
687 |
||
57650 | 688 |
* Fact collections add_ac and mult_ac are considered old-fashioned. |
57637
eeb2d50ec71f
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
wenzelm
parents:
57594
diff
changeset
|
689 |
Prefer ac_simps instead, or specify rules |
eeb2d50ec71f
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
wenzelm
parents:
57594
diff
changeset
|
690 |
(add|mult).(assoc|commute|left_commute) individually. |
57517 | 691 |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
692 |
* Elimination of fact duplicates: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
693 |
equals_zero_I ~> minus_unique |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
694 |
diff_eq_0_iff_eq ~> right_minus_eq |
54588 | 695 |
nat_infinite ~> infinite_UNIV_nat |
696 |
int_infinite ~> infinite_UNIV_int |
|
57452 | 697 |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
698 |
INCOMPATIBILITY. |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
699 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
700 |
* Fact name consolidation: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
701 |
diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus |
54250 | 702 |
minus_le_self_iff ~> neg_less_eq_nonneg |
703 |
le_minus_self_iff ~> less_eq_neg_nonpos |
|
704 |
neg_less_nonneg ~> neg_less_pos |
|
705 |
less_minus_self_iff ~> less_neg_neg [simp] |
|
57452 | 706 |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
707 |
INCOMPATIBILITY. |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
708 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
709 |
* More simplification rules on unary and binary minus: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
710 |
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
|
711 |
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
|
712 |
add_minus_cancel, diff_add_cancel, le_add_same_cancel1, |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
713 |
le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2, |
57452 | 714 |
minus_add_cancel, uminus_add_conv_diff. These correspondingly have |
715 |
been taken away from fact collections algebra_simps and field_simps. |
|
716 |
INCOMPATIBILITY. |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
717 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
718 |
To restore proofs, the following patterns are helpful: |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
719 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
720 |
a) Arbitrary failing proof not involving "diff_def": |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
721 |
Consider simplification with algebra_simps or field_simps. |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
722 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
723 |
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
|
724 |
Try with "using <rule for addition> of [... "- _" ...]" by simp". |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
725 |
|
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
726 |
c) Simplification with "diff_def": just drop "diff_def". |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
727 |
Consider simplification with algebra_simps or field_simps; |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
728 |
or the brute way with |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset
|
729 |
"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
|
730 |
|
57452 | 731 |
* Introduce bdd_above and bdd_below in theory |
732 |
Conditionally_Complete_Lattices, use them instead of explicitly |
|
733 |
stating boundedness of sets. |
|
734 |
||
735 |
* ccpo.admissible quantifies only over non-empty chains to allow more |
|
736 |
syntax-directed proof rules; the case of the empty chain shows up as |
|
737 |
additional case in fixpoint induction proofs. INCOMPATIBILITY. |
|
54264 | 738 |
|
56214 | 739 |
* Removed and renamed theorems in Series: |
740 |
summable_le ~> suminf_le |
|
741 |
suminf_le ~> suminf_le_const |
|
742 |
series_pos_le ~> setsum_le_suminf |
|
743 |
series_pos_less ~> setsum_less_suminf |
|
744 |
suminf_ge_zero ~> suminf_nonneg |
|
745 |
suminf_gt_zero ~> suminf_pos |
|
746 |
suminf_gt_zero_iff ~> suminf_pos_iff |
|
747 |
summable_sumr_LIMSEQ_suminf ~> summable_LIMSEQ |
|
748 |
suminf_0_le ~> suminf_nonneg [rotate] |
|
749 |
pos_summable ~> summableI_nonneg_bounded |
|
750 |
ratio_test ~> summable_ratio_test |
|
751 |
||
752 |
removed series_zero, replaced by sums_finite |
|
753 |
||
754 |
removed auxiliary lemmas: |
|
57452 | 755 |
|
56214 | 756 |
sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group, |
57452 | 757 |
half, le_Suc_ex_iff, lemma_realpow_diff_sumr, |
758 |
real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2, |
|
759 |
sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero, |
|
760 |
summable_convergent_sumr_iff, sumr_diff_mult_const |
|
761 |
||
56214 | 762 |
INCOMPATIBILITY. |
763 |
||
764 |
* Replace (F)DERIV syntax by has_derivative: |
|
765 |
- "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'" |
|
766 |
||
767 |
- "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'" |
|
768 |
||
769 |
- "f differentiable at x within s" replaces "_ differentiable _ in _" syntax |
|
770 |
||
771 |
- removed constant isDiff |
|
772 |
||
57452 | 773 |
- "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as |
774 |
input syntax. |
|
775 |
||
776 |
- "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed. |
|
56214 | 777 |
|
778 |
- Renamed FDERIV_... lemmas to has_derivative_... |
|
779 |
||
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
780 |
- renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
781 |
|
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
782 |
- removed DERIV_intros, has_derivative_eq_intros |
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
783 |
|
57452 | 784 |
- introduced derivative_intros and deriative_eq_intros which |
785 |
includes now rules for DERIV, has_derivative and |
|
786 |
has_vector_derivative. |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
787 |
|
56214 | 788 |
- Other renamings: |
789 |
differentiable_def ~> real_differentiable_def |
|
790 |
differentiableE ~> real_differentiableE |
|
791 |
fderiv_def ~> has_derivative_at |
|
792 |
field_fderiv_def ~> field_has_derivative_at |
|
793 |
isDiff_der ~> differentiable_def |
|
794 |
deriv_fderiv ~> has_field_derivative_def |
|
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset
|
795 |
deriv_def ~> DERIV_def |
57452 | 796 |
|
797 |
INCOMPATIBILITY. |
|
798 |
||
799 |
* Include more theorems in continuous_intros. Remove the |
|
800 |
continuous_on_intros, isCont_intros collections, these facts are now |
|
801 |
in continuous_intros. |
|
802 |
||
803 |
* Theorems about complex numbers are now stated only using Re and Im, |
|
804 |
the Complex constructor is not used anymore. It is possible to use |
|
805 |
primcorec to defined the behaviour of a complex-valued function. |
|
806 |
||
807 |
Removed theorems about the Complex constructor from the simpset, they |
|
808 |
are available as the lemma collection legacy_Complex_simps. This |
|
809 |
especially removes |
|
810 |
||
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
811 |
i_complex_of_real: "ii * complex_of_real r = Complex 0 r". |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
812 |
|
57452 | 813 |
Instead the reverse direction is supported with |
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
814 |
Complex_eq: "Complex a b = a + \<i> * b" |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
815 |
|
57452 | 816 |
Moved csqrt from Fundamental_Algebra_Theorem to Complex. |
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
817 |
|
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
818 |
Renamings: |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
819 |
Re/Im ~> complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
820 |
complex_Re/Im_zero ~> zero_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
821 |
complex_Re/Im_add ~> plus_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
822 |
complex_Re/Im_minus ~> uminus_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
823 |
complex_Re/Im_diff ~> minus_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
824 |
complex_Re/Im_one ~> one_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
825 |
complex_Re/Im_mult ~> times_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
826 |
complex_Re/Im_inverse ~> inverse_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
827 |
complex_Re/Im_scaleR ~> scaleR_complex.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
828 |
complex_Re/Im_i ~> ii.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
829 |
complex_Re/Im_cnj ~> cnj.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
830 |
Re/Im_cis ~> cis.sel |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
831 |
|
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
832 |
complex_divide_def ~> divide_complex_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
833 |
complex_norm_def ~> norm_complex_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
834 |
cmod_def ~> norm_complex_de |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
835 |
|
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
836 |
Removed theorems: |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
837 |
complex_zero_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
838 |
complex_add_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
839 |
complex_minus_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
840 |
complex_diff_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
841 |
complex_one_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
842 |
complex_mult_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
843 |
complex_inverse_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
844 |
complex_scaleR_def |
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset
|
845 |
|
57452 | 846 |
INCOMPATIBILITY. |
847 |
||
57504 | 848 |
* Theory Lubs moved HOL image to HOL-Library. It is replaced by |
849 |
Conditionally_Complete_Lattices. INCOMPATIBILITY. |
|
850 |
||
851 |
* HOL-Library: new theory src/HOL/Library/Tree.thy. |
|
852 |
||
853 |
* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it |
|
854 |
is subsumed by session Kleene_Algebra in AFP. |
|
855 |
||
57856 | 856 |
* HOL-Library / theory RBT: various constants and facts are hidden; |
857 |
lifting setup is unregistered. INCOMPATIBILITY. |
|
57826 | 858 |
|
57504 | 859 |
* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. |
860 |
||
861 |
* HOL-Word: bit representations prefer type bool over type bit. |
|
862 |
INCOMPATIBILITY. |
|
863 |
||
864 |
* HOL-Word: |
|
865 |
- Abandoned fact collection "word_arith_alts", which is a duplicate |
|
866 |
of "word_arith_wis". |
|
867 |
- Dropped first (duplicated) element in fact collections |
|
868 |
"sint_word_ariths", "word_arith_alts", "uint_word_ariths", |
|
869 |
"uint_word_arith_bintrs". |
|
870 |
||
871 |
* HOL-Number_Theory: |
|
872 |
- consolidated the proofs of the binomial theorem |
|
873 |
- the function fib is again of type nat => nat and not overloaded |
|
874 |
- no more references to Old_Number_Theory in the HOL libraries |
|
875 |
(except the AFP) |
|
876 |
||
877 |
INCOMPATIBILITY. |
|
878 |
||
54787 | 879 |
* HOL-Multivariate_Analysis: |
57452 | 880 |
- Type class ordered_real_vector for ordered vector spaces. |
881 |
- New theory Complex_Basic_Analysis defining complex derivatives, |
|
57253 | 882 |
holomorphic functions, etc., ported from HOL Light's canal.ml. |
57452 | 883 |
- Changed order of ordered_euclidean_space to be compatible with |
54787 | 884 |
pointwise ordering on products. Therefore instance of |
885 |
conditionally_complete_lattice and ordered_real_vector. |
|
886 |
INCOMPATIBILITY: use box instead of greaterThanLessThan or |
|
57452 | 887 |
explicit set-comprehensions with eucl_less for other (half-)open |
54787 | 888 |
intervals. |
57476 | 889 |
- removed dependencies on type class ordered_euclidean_space with |
890 |
introduction of "cbox" on euclidean_space |
|
891 |
- renamed theorems: |
|
892 |
interval ~> box |
|
893 |
mem_interval ~> mem_box |
|
894 |
interval_eq_empty ~> box_eq_empty |
|
895 |
interval_ne_empty ~> box_ne_empty |
|
896 |
interval_sing(1) ~> cbox_sing |
|
897 |
interval_sing(2) ~> box_sing |
|
898 |
subset_interval_imp ~> subset_box_imp |
|
899 |
subset_interval ~> subset_box |
|
900 |
open_interval ~> open_box |
|
901 |
closed_interval ~> closed_cbox |
|
902 |
interior_closed_interval ~> interior_cbox |
|
903 |
bounded_closed_interval ~> bounded_cbox |
|
904 |
compact_interval ~> compact_cbox |
|
905 |
bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric |
|
906 |
bounded_subset_closed_interval ~> bounded_subset_cbox |
|
907 |
mem_interval_componentwiseI ~> mem_box_componentwiseI |
|
908 |
convex_box ~> convex_prod |
|
909 |
rel_interior_real_interval ~> rel_interior_real_box |
|
910 |
convex_interval ~> convex_box |
|
911 |
convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox |
|
912 |
frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox |
|
913 |
content_closed_interval' ~> content_cbox' |
|
914 |
elementary_subset_interval ~> elementary_subset_box |
|
915 |
diameter_closed_interval ~> diameter_cbox |
|
916 |
frontier_closed_interval ~> frontier_cbox |
|
917 |
frontier_open_interval ~> frontier_box |
|
918 |
bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric |
|
919 |
closure_open_interval ~> closure_box |
|
920 |
open_closed_interval_convex ~> open_cbox_convex |
|
921 |
open_interval_midpoint ~> box_midpoint |
|
922 |
content_image_affinity_interval ~> content_image_affinity_cbox |
|
923 |
is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval |
|
924 |
bounded_interval ~> bounded_closed_interval + bounded_boxes |
|
925 |
||
926 |
- respective theorems for intervals over the reals: |
|
927 |
content_closed_interval + content_cbox |
|
928 |
has_integral + has_integral_real |
|
929 |
fine_division_exists + fine_division_exists_real |
|
930 |
has_integral_null + has_integral_null_real |
|
931 |
tagged_division_union_interval + tagged_division_union_interval_real |
|
932 |
has_integral_const + has_integral_const_real |
|
933 |
integral_const + integral_const_real |
|
934 |
has_integral_bound + has_integral_bound_real |
|
935 |
integrable_continuous + integrable_continuous_real |
|
936 |
integrable_subinterval + integrable_subinterval_real |
|
937 |
has_integral_reflect_lemma + has_integral_reflect_lemma_real |
|
938 |
integrable_reflect + integrable_reflect_real |
|
939 |
integral_reflect + integral_reflect_real |
|
940 |
image_affinity_interval + image_affinity_cbox |
|
941 |
image_smult_interval + image_smult_cbox |
|
942 |
integrable_const + integrable_const_ivl |
|
943 |
integrable_on_subinterval + integrable_on_subcbox |
|
944 |
||
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset
|
945 |
- renamed theorems: |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset
|
946 |
derivative_linear ~> has_derivative_bounded_linear |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset
|
947 |
derivative_is_linear ~> has_derivative_linear |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset
|
948 |
bounded_linear_imp_linear ~> bounded_linear.linear |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset
|
949 |
|
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
950 |
* HOL-Probability: |
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
951 |
- Renamed positive_integral to nn_integral: |
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
952 |
|
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
953 |
. Renamed all lemmas "*positive_integral*" to *nn_integral*" |
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
954 |
positive_integral_positive ~> nn_integral_nonneg |
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
955 |
|
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
956 |
. Renamed abbreviation integral\<^sup>P to integral\<^sup>N. |
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
957 |
|
57452 | 958 |
- replaced the Lebesgue integral on real numbers by the more general |
959 |
Bochner integral for functions into a real-normed vector space. |
|
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
960 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
961 |
integral_zero ~> integral_zero / integrable_zero |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
962 |
integral_minus ~> integral_minus / integrable_minus |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
963 |
integral_add ~> integral_add / integrable_add |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
964 |
integral_diff ~> integral_diff / integrable_diff |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
965 |
integral_setsum ~> integral_setsum / integrable_setsum |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
966 |
integral_multc ~> integral_mult_left / integrable_mult_left |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
967 |
integral_cmult ~> integral_mult_right / integrable_mult_right |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
968 |
integral_triangle_inequality~> integral_norm_bound |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
969 |
integrable_nonneg ~> integrableI_nonneg |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
970 |
integral_positive ~> integral_nonneg_AE |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
971 |
integrable_abs_iff ~> integrable_abs_cancel |
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
972 |
positive_integral_lim_INF ~> nn_integral_liminf |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
973 |
lebesgue_real_affine ~> lborel_real_affine |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
974 |
borel_integral_has_integral ~> has_integral_lebesgue_integral |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
975 |
integral_indicator ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
976 |
integral_real_indicator / integrable_real_indicator |
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
977 |
positive_integral_fst ~> nn_integral_fst' |
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
978 |
positive_integral_fst_measurable ~> nn_integral_fst |
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
979 |
positive_integral_snd_measurable ~> nn_integral_snd |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
980 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
981 |
integrable_fst_measurable ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
982 |
integral_fst / integrable_fst / AE_integrable_fst |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
983 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
984 |
integrable_snd_measurable ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
985 |
integral_snd / integrable_snd / AE_integrable_snd |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
986 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
987 |
integral_monotone_convergence ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
988 |
integral_monotone_convergence / integrable_monotone_convergence |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
989 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
990 |
integral_monotone_convergence_at_top ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
991 |
integral_monotone_convergence_at_top / |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
992 |
integrable_monotone_convergence_at_top |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
993 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
994 |
has_integral_iff_positive_integral_lebesgue ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
995 |
has_integral_iff_has_bochner_integral_lebesgue_nonneg |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
996 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
997 |
lebesgue_integral_has_integral ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
998 |
has_integral_integrable_lebesgue_nonneg |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
999 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1000 |
positive_integral_lebesgue_has_integral ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1001 |
integral_has_integral_lebesgue_nonneg / |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1002 |
integrable_has_integral_lebesgue_nonneg |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1003 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1004 |
lebesgue_integral_real_affine ~> |
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset
|
1005 |
nn_integral_real_affine |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1006 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1007 |
has_integral_iff_positive_integral_lborel ~> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1008 |
integral_has_integral_nonneg / integrable_has_integral_nonneg |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1009 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1010 |
The following theorems where removed: |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1011 |
|
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1012 |
lebesgue_integral_nonneg |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1013 |
lebesgue_integral_uminus |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1014 |
lebesgue_integral_cmult |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1015 |
lebesgue_integral_multc |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1016 |
lebesgue_integral_cmult_nonneg |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1017 |
integral_cmul_indicator |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
56964
diff
changeset
|
1018 |
integral_real |
54672
748778ac0ab8
relocate NEWS to post-release version (cf. 7a14f831d02d);
wenzelm
parents:
54671
diff
changeset
|
1019 |
|
57452 | 1020 |
- Formalized properties about exponentially, Erlang, and normal |
1021 |
distributed random variables. |
|
1022 |
||
57504 | 1023 |
* HOL-Decision_Procs: Separate command 'approximate' for approximative |
1024 |
computation in src/HOL/Decision_Procs/Approximation. Minor |
|
1025 |
INCOMPATIBILITY. |
|
57452 | 1026 |
|
57112
70395c65c0e3
removed Kleene_Algebra because of superior AFP entry; authors agreed
nipkow
parents:
57094
diff
changeset
|
1027 |
|
55622
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
1028 |
*** Scala *** |
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
1029 |
|
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
1030 |
* 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
|
1031 |
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
|
1032 |
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
|
1033 |
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
|
1034 |
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
|
1035 |
|
57452 | 1036 |
* Substantial reworking of internal PIDE protocol communication |
1037 |
channels. INCOMPATIBILITY. |
|
1038 |
||
55622
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset
|
1039 |
|
54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
1040 |
*** ML *** |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
1041 |
|
57504 | 1042 |
* Subtle change of semantics of Thm.eq_thm: theory stamps are not |
1043 |
compared (according to Thm.thm_ord), but assumed to be covered by the |
|
1044 |
current background theory. Thus equivalent data produced in different |
|
1045 |
branches of the theory graph usually coincides (e.g. relevant for |
|
1046 |
theory merge). Note that the softer Thm.eq_thm_prop is often more |
|
1047 |
appropriate than Thm.eq_thm. |
|
1048 |
||
1049 |
* Proper context for basic Simplifier operations: rewrite_rule, |
|
1050 |
rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to |
|
1051 |
pass runtime Proof.context (and ensure that the simplified entity |
|
1052 |
actually belongs to it). |
|
1053 |
||
1054 |
* Proper context discipline for read_instantiate and instantiate_tac: |
|
1055 |
variables that are meant to become schematic need to be given as |
|
1056 |
fixed, and are generalized by the explicit context of local variables. |
|
1057 |
This corresponds to Isar attributes "where" and "of" with 'for' |
|
1058 |
declaration. INCOMPATIBILITY, also due to potential change of indices |
|
1059 |
of schematic variables. |
|
1060 |
||
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56285
diff
changeset
|
1061 |
* Moved ML_Compiler.exn_trace and other operations on exceptions to |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56285
diff
changeset
|
1062 |
structure Runtime. Minor INCOMPATIBILITY. |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56285
diff
changeset
|
1063 |
|
56279
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56276
diff
changeset
|
1064 |
* Discontinued old Toplevel.debug in favour of system option |
57452 | 1065 |
"ML_exception_trace", which may be also declared within the context |
1066 |
via "declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY. |
|
56279
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56276
diff
changeset
|
1067 |
|
56281 | 1068 |
* Renamed configuration option "ML_trace" to "ML_source_trace". Minor |
1069 |
INCOMPATIBILITY. |
|
1070 |
||
1071 |
* Configuration option "ML_print_depth" controls the pretty-printing |
|
1072 |
depth of the ML compiler within the context. The old print_depth in |
|
56285 | 1073 |
ML is still available as default_print_depth, but rarely used. Minor |
1074 |
INCOMPATIBILITY. |
|
56279
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56276
diff
changeset
|
1075 |
|
54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
1076 |
* Toplevel function "use" refers to raw ML bootstrap environment, |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
1077 |
without Isar context nor antiquotations. Potential INCOMPATIBILITY. |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
1078 |
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
|
1079 |
formal context. |
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
1080 |
|
56205 | 1081 |
* Simplified programming interface to define ML antiquotations, see |
1082 |
structure ML_Antiquotation. Minor INCOMPATIBILITY. |
|
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55965
diff
changeset
|
1083 |
|
56071 | 1084 |
* ML antiquotation @{here} refers to its source position, which is |
1085 |
occasionally useful for experimentation and diagnostic purposes. |
|
1086 |
||
56135 | 1087 |
* ML antiquotation @{path} produces a Path.T value, similarly to |
1088 |
Path.explode, but with compile-time check against the file-system and |
|
1089 |
some PIDE markup. Note that unlike theory source, ML does not have a |
|
1090 |
well-defined master directory, so an absolute symbolic path |
|
1091 |
specification is usually required, e.g. "~~/src/HOL". |
|
1092 |
||
56399 | 1093 |
* ML antiquotation @{print} inlines a function to print an arbitrary |
1094 |
ML value, which is occasionally useful for diagnostic or demonstration |
|
1095 |
purposes. |
|
1096 |
||
54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset
|
1097 |
|
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
1098 |
*** System *** |
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
54672
diff
changeset
|
1099 |
|
57443
577f029fde39
ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
wenzelm
parents:
57439
diff
changeset
|
1100 |
* Proof General with its traditional helper scripts is now an optional |
57504 | 1101 |
Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle |
1102 |
component repository http://isabelle.in.tum.de/components/. Note that |
|
1103 |
the "system" manual provides general explanations about add-on |
|
1104 |
components, especially those that are not bundled with the release. |
|
57443
577f029fde39
ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
wenzelm
parents:
57439
diff
changeset
|
1105 |
|
56439
95e2656b3b23
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
56413
diff
changeset
|
1106 |
* The raw Isabelle process executable has been renamed from |
95e2656b3b23
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
56413
diff
changeset
|
1107 |
"isabelle-process" to "isabelle_process", which conforms to common |
95e2656b3b23
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
56413
diff
changeset
|
1108 |
shell naming conventions, and allows to define a shell function within |
95e2656b3b23
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
56413
diff
changeset
|
1109 |
the Isabelle environment to avoid dynamic path lookup. Rare |
57504 | 1110 |
incompatibility for old tools that do not use the ISABELLE_PROCESS |
1111 |
settings variable. |
|
56439
95e2656b3b23
renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
wenzelm
parents:
56413
diff
changeset
|
1112 |
|
57439
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57437
diff
changeset
|
1113 |
* Former "isabelle tty" has been superseded by "isabelle console", |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57437
diff
changeset
|
1114 |
with implicit build like "isabelle jedit", and without the mostly |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57437
diff
changeset
|
1115 |
obsolete Isar TTY loop. |
0e41f26a0250
"isabelle tty" is superseded by "isabelle console";
wenzelm
parents:
57437
diff
changeset
|
1116 |
|
57452 | 1117 |
* Simplified "isabelle display" tool. Settings variables DVI_VIEWER |
1118 |
and PDF_VIEWER now refer to the actual programs, not shell |
|
1119 |
command-lines. Discontinued option -c: invocation may be asynchronous |
|
1120 |
via desktop environment, without any special precautions. Potential |
|
1121 |
INCOMPATIBILITY with ambitious private settings. |
|
1122 |
||
57413 | 1123 |
* Removed obsolete "isabelle unsymbolize". Note that the usual format |
1124 |
for email communication is the Unicode rendering of Isabelle symbols, |
|
1125 |
as produced by Isabelle/jEdit, for example. |
|
1126 |
||
57452 | 1127 |
* Removed obsolete tool "wwwfind". Similar functionality may be |
1128 |
integrated into Isabelle/jEdit eventually. |
|
1129 |
||
1130 |
* Improved 'display_drafts' concerning desktop integration and |
|
1131 |
repeated invocation in PIDE front-end: re-use single file |
|
1132 |
$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views. |
|
57084 | 1133 |
|
57452 | 1134 |
* Session ROOT specifications require explicit 'document_files' for |
1135 |
robust dependencies on LaTeX sources. Only these explicitly given |
|
1136 |
files are copied to the document output directory, before document |
|
1137 |
processing is started. |
|
1138 |
||
57504 | 1139 |
* Windows: support for regular TeX installation (e.g. MiKTeX) instead |
1140 |
of TeX Live from Cygwin. |
|
1141 |
||
57084 | 1142 |
|
57693 | 1143 |
|
54639 | 1144 |
New in Isabelle2013-2 (December 2013) |
1145 |
------------------------------------- |
|
1146 |
||
1147 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
|
1148 |
||
1149 |
* More robust editing of running commands with internal forks, |
|
1150 |
e.g. non-terminating 'by' steps. |
|
1151 |
||
54641 | 1152 |
* More relaxed Sledgehammer panel: avoid repeated application of query |
1153 |
after edits surrounding the command location. |
|
1154 |
||
54648 | 1155 |
* More status information about commands that are interrupted |
1156 |
accidentally (via physical event or Poly/ML runtime system signal, |
|
1157 |
e.g. out-of-memory). |
|
1158 |
||
54653 | 1159 |
|
1160 |
*** System *** |
|
1161 |
||
1162 |
* More robust termination of external processes managed by |
|
54664 | 1163 |
Isabelle/ML: support cancellation of tasks within the range of |
1164 |
milliseconds, as required for PIDE document editing with automatically |
|
1165 |
tried tools (e.g. Sledgehammer). |
|
54653 | 1166 |
|
54648 | 1167 |
* Reactivated Isabelle/Scala kill command for external processes on |
1168 |
Mac OS X, which was accidentally broken in Isabelle2013-1 due to a |
|
1169 |
workaround for some Debian/Ubuntu Linux versions from 2013. |
|
1170 |
||
54639 | 1171 |
|
1172 |
||
53971 | 1173 |
New in Isabelle2013-1 (November 2013) |
1174 |
------------------------------------- |
|
50994 | 1175 |
|
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
1176 |
*** General *** |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
1177 |
|
53971 | 1178 |
* Discontinued obsolete 'uses' within theory header. Note that |
1179 |
commands like 'ML_file' work without separate declaration of file |
|
1180 |
dependencies. Minor INCOMPATIBILITY. |
|
1181 |
||
1182 |
* Discontinued redundant 'use' command, which was superseded by |
|
1183 |
'ML_file' in Isabelle2013. Minor INCOMPATIBILITY. |
|
1184 |
||
53016
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
1185 |
* 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
|
1186 |
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
|
1187 |
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
|
1188 |
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
|
1189 |
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
|
1190 |
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
|
1191 |
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
|
1192 |
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
|
1193 |
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
|
1194 |
syntax. |
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents:
52949
diff
changeset
|
1195 |
|
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
53016
diff
changeset
|
1196 |
* 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
|
1197 |
"sub". Minor INCOMPATIBILITY. |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
53016
diff
changeset
|
1198 |
|
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
1199 |
* 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
|
1200 |
"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
|
1201 |
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
|
1202 |
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
|
1203 |
quick_and_dirty, instead of historical poking into mutable reference. |
52059 | 1204 |
|
52060 | 1205 |
* Renamed command 'print_configs' to 'print_options'. Minor |
1206 |
INCOMPATIBILITY. |
|
1207 |
||
52430 | 1208 |
* Proper diagnostic command 'print_state'. Old 'pr' (with its |
1209 |
implicit change of some global references) is retained for now as |
|
1210 |
control command, e.g. for ProofGeneral 3.7.x. |
|
1211 |
||
52549 | 1212 |
* Discontinued 'print_drafts' command with its old-fashioned PS output |
1213 |
and Unix command-line print spooling. Minor INCOMPATIBILITY: use |
|
1214 |
'display_drafts' instead and print via the regular document viewer. |
|
1215 |
||
53971 | 1216 |
* Updated and extended "isar-ref" and "implementation" manual, |
1217 |
eliminated old "ref" manual. |
|
1218 |
||
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
1219 |
|
51533 | 1220 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
1221 |
||
53971 | 1222 |
* New manual "jedit" for Isabelle/jEdit, see isabelle doc or |
53852 | 1223 |
Documentation panel. |
1224 |
||
53971 | 1225 |
* Dockable window "Documentation" provides access to Isabelle |
1226 |
documentation. |
|
52646 | 1227 |
|
52949 | 1228 |
* Dockable window "Find" provides query operations for formal entities |
1229 |
(GUI front-end to 'find_theorems' command). |
|
1230 |
||
53050 | 1231 |
* Dockable window "Sledgehammer" manages asynchronous / parallel |
1232 |
sledgehammer runs over existing document sources, independently of |
|
1233 |
normal editing and checking process. |
|
1234 |
||
51533 | 1235 |
* Dockable window "Timing" provides an overview of relevant command |
54332 | 1236 |
timing information, depending on option jedit_timing_threshold. The |
1237 |
same timing information is shown in the extended tooltip of the |
|
1238 |
command keyword, when hovering the mouse over it while the CONTROL or |
|
1239 |
COMMAND modifier is pressed. |
|
51533 | 1240 |
|
53971 | 1241 |
* Improved dockable window "Theories": Continuous checking of proof |
1242 |
document (visible and required parts) may be controlled explicitly, |
|
1243 |
using check box or shortcut "C+e ENTER". Individual theory nodes may |
|
1244 |
be marked explicitly as required and checked in full, using check box |
|
1245 |
or shortcut "C+e SPACE". |
|
1246 |
||
54305 | 1247 |
* Improved completion mechanism, which is now managed by the |
1248 |
Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle |
|
1249 |
symbol abbreviations (see $ISABELLE_HOME/etc/symbols). |
|
1250 |
||
54319 | 1251 |
* Standard jEdit keyboard shortcut C+b complete-word is remapped to |
1252 |
isabelle.complete for explicit completion in Isabelle sources. |
|
1253 |
INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts |
|
1254 |
to resolve conflict. |
|
1255 |
||
54305 | 1256 |
* Improved support of various "minor modes" for Isabelle NEWS, |
1257 |
options, session ROOT etc., with completion and SideKick tree view. |
|
1258 |
||
53971 | 1259 |
* Strictly monotonic document update, without premature cancellation of |
1260 |
running transactions that are still needed: avoid reset/restart of |
|
1261 |
such command executions while editing. |
|
53271
0460d6962ced
GTK+ works better due to avoidance of default list view popups;
wenzelm
parents:
53251
diff
changeset
|
1262 |
|
53971 | 1263 |
* Support for asynchronous print functions, as overlay to existing |
1264 |
document content. |
|
1265 |
||
1266 |
* Support for automatic tools in HOL, which try to prove or disprove |
|
1267 |
toplevel theorem statements. |
|
1268 |
||
1269 |
* 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
|
1270 |
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
|
1271 |
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
|
1272 |
keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0). |
53971 | 1273 |
|
1274 |
* File specifications in jEdit (e.g. file browser) may refer to |
|
54351 | 1275 |
$ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms. Discontinued |
1276 |
obsolete $ISABELLE_HOME_WINDOWS variable. |
|
53971 | 1277 |
|
1278 |
* Improved support for Linux look-and-feel "GTK+", see also "Utilities |
|
1279 |
/ Global Options / Appearance". |
|
1280 |
||
1281 |
* Improved support of native Mac OS X functionality via "MacOSX" |
|
1282 |
plugin, which is now enabled by default. |
|
1283 |
||
51533 | 1284 |
|
51313 | 1285 |
*** Pure *** |
1286 |
||
54049 | 1287 |
* Commands 'interpretation' and 'sublocale' are now target-sensitive. |
1288 |
In particular, 'interpretation' allows for non-persistent |
|
1289 |
interpretation within "context ... begin ... end" blocks offering a |
|
1290 |
light-weight alternative to 'sublocale'. See "isar-ref" manual for |
|
1291 |
details. |
|
51747 | 1292 |
|
51565 | 1293 |
* Improved locales diagnostic command 'print_dependencies'. |
1294 |
||
51313 | 1295 |
* Discontinued obsolete 'axioms' command, which has been marked as |
1296 |
legacy since Isabelle2009-2. INCOMPATIBILITY, use 'axiomatization' |
|
1297 |
instead, while observing its uniform scope for polymorphism. |
|
1298 |
||
51316
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
1299 |
* Discontinued empty name bindings in 'axiomatization'. |
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
1300 |
INCOMPATIBILITY. |
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
1301 |
|
53971 | 1302 |
* System option "proofs" has been discontinued. Instead the global |
1303 |
state of Proofterm.proofs is persistently compiled into logic images |
|
1304 |
as required, notably HOL-Proofs. Users no longer need to change |
|
1305 |
Proofterm.proofs dynamically. Minor INCOMPATIBILITY. |
|
1306 |
||
1307 |
* Syntax translation functions (print_translation etc.) always depend |
|
1308 |
on Proof.context. Discontinued former "(advanced)" option -- this is |
|
1309 |
now the default. Minor INCOMPATIBILITY. |
|
1310 |
||
1311 |
* Former global reference trace_unify_fail is now available as |
|
1312 |
configuration option "unify_trace_failure" (global context only). |
|
1313 |
||
52463 | 1314 |
* SELECT_GOAL now retains the syntactic context of the overall goal |
1315 |
state (schematic variables etc.). Potential INCOMPATIBILITY in rare |
|
1316 |
situations. |
|
1317 |
||
51313 | 1318 |
|
51002
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
1319 |
*** HOL *** |
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
1320 |
|
54032 | 1321 |
* Stronger precedence of syntax for big intersection and union on |
1322 |
sets, in accordance with corresponding lattice operations. |
|
1323 |
INCOMPATIBILITY. |
|
1324 |
||
1325 |
* Notation "{p:A. P}" now allows tuple patterns as well. |
|
1326 |
||
1327 |
* Nested case expressions are now translated in a separate check phase |
|
1328 |
rather than during parsing. The data for case combinators is separated |
|
1329 |
from the datatype package. The declaration attribute |
|
1330 |
"case_translation" can be used to register new case combinators: |
|
1331 |
||
1332 |
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
|
1333 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
1334 |
* Code generator: |
53160 | 1335 |
- 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / |
1336 |
'code_instance'. |
|
1337 |
- 'code_identifier' declares name hints for arbitrary identifiers in |
|
1338 |
generated code, subsuming 'code_modulename'. |
|
53983 | 1339 |
|
1340 |
See the isar-ref manual for syntax diagrams, and the HOL theories for |
|
1341 |
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
|
1342 |
|
54032 | 1343 |
* Attibute 'code': 'code' now declares concrete and abstract code |
1344 |
equations uniformly. Use explicit 'code equation' and 'code abstract' |
|
1345 |
to distinguish both when desired. |
|
1346 |
||
1347 |
* Discontinued theories Code_Integer and Efficient_Nat by a more |
|
1348 |
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat, |
|
1349 |
Code_Target_Nat and Code_Target_Numeral. See the tutorial on code |
|
1350 |
generation for details. INCOMPATIBILITY. |
|
1351 |
||
1352 |
* Numeric types are mapped by default to target language numerals: |
|
1353 |
natural (replaces former code_numeral) and integer (replaces former |
|
1354 |
code_int). Conversions are available as integer_of_natural / |
|
1355 |
natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and |
|
1356 |
Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in |
|
1357 |
ML). INCOMPATIBILITY. |
|
1358 |
||
1359 |
* Function package: For mutually recursive functions f and g, separate |
|
1360 |
cases rules f.cases and g.cases are generated instead of unusable |
|
1361 |
f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY, |
|
1362 |
in the case that the unusable rule was used nevertheless. |
|
1363 |
||
1364 |
* Function package: For each function f, new rules f.elims are |
|
1365 |
generated, which eliminate equalities of the form "f x = t". |
|
1366 |
||
1367 |
* New command 'fun_cases' derives ad-hoc elimination rules for |
|
1368 |
function equations as simplified instances of f.elims, analogous to |
|
1369 |
inductive_cases. See ~~/src/HOL/ex/Fundefs.thy for some examples. |
|
53307 | 1370 |
|
54021 | 1371 |
* Lifting: |
1372 |
- parametrized correspondence relations are now supported: |
|
54378 | 1373 |
+ parametricity theorems for the raw term can be specified in |
54021 | 1374 |
the command lift_definition, which allow us to generate stronger |
1375 |
transfer rules |
|
1376 |
+ setup_lifting generates stronger transfer rules if parametric |
|
1377 |
correspondence relation can be generated |
|
1378 |
+ various new properties of the relator must be specified to support |
|
1379 |
parametricity |
|
1380 |
+ parametricity theorem for the Quotient relation can be specified |
|
1381 |
- setup_lifting generates domain rules for the Transfer package |
|
1382 |
- stronger reflexivity prover of respectfulness theorems for type |
|
1383 |
copies |
|
1384 |
- ===> and --> are now local. The symbols can be introduced |
|
1385 |
by interpreting the locale lifting_syntax (typically in an |
|
1386 |
anonymous context) |
|
54378 | 1387 |
- Lifting/Transfer relevant parts of Library/Quotient_* are now in |
54021 | 1388 |
Main. Potential INCOMPATIBILITY |
1389 |
- new commands for restoring and deleting Lifting/Transfer context: |
|
1390 |
lifting_forget, lifting_update |
|
54378 | 1391 |
- the command print_quotmaps was renamed to print_quot_maps. |
54021 | 1392 |
INCOMPATIBILITY |
1393 |
||
1394 |
* Transfer: |
|
54378 | 1395 |
- better support for domains in Transfer: replace Domainp T |
54021 | 1396 |
by the actual invariant in a transferred goal |
1397 |
- transfer rules can have as assumptions other transfer rules |
|
1398 |
- Experimental support for transferring from the raw level to the |
|
1399 |
abstract level: Transfer.transferred attribute |
|
1400 |
- Attribute version of the transfer method: untransferred attribute |
|
1401 |
||
52286 | 1402 |
* Reification and reflection: |
53160 | 1403 |
- Reification is now directly available in HOL-Main in structure |
1404 |
"Reification". |
|
1405 |
- Reflection now handles multiple lists with variables also. |
|
1406 |
- The whole reflection stack has been decomposed into conversions. |
|
52286 | 1407 |
INCOMPATIBILITY. |
1408 |
||
51489 | 1409 |
* Revised devices for recursive definitions over finite sets: |
1410 |
- Only one fundamental fold combinator on finite set remains: |
|
1411 |
Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b |
|
1412 |
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
|
1413 |
- Locales ("mini packages") for fundamental definitions with |
51489 | 1414 |
Finite_Set.fold: folding, folding_idem. |
1415 |
- Locales comm_monoid_set, semilattice_order_set and |
|