author  wenzelm 
Mon, 23 Mar 2015 23:16:40 +0100  
changeset 59792  f19f4afa49e2 
parent 59751  916c0f6c83e3 
child 59796  f05ef8c62e4f 
permissions  rwrr 
57491  1 
Isabelle NEWS  history of userrelevant 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 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59648
diff
changeset

9 
* Structural composition of proof methods (meth1; meth2) in Isar 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59648
diff
changeset

10 
corresponds to (tac1 THEN_ALL_NEW tac2) in ML. 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59648
diff
changeset

11 

59648  12 
* Generated schematic variables in standard format of exported facts are 
13 
incremented to avoid material in the proof context. Rare 

14 
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to 

15 
different index. 

16 

59569  17 
* Commands 'method_setup' and 'attribute_setup' now work within a local 
18 
theory context. 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

19 

57946
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset

20 
* Command 'named_theorems' declares a dynamic fact within the context, 
59569  21 
together with an attribute to maintain the content incrementally. This 
22 
supersedes functor Named_Thms, but with a subtle change of semantics due 

23 
to external visual order vs. internal reverse order. 

57946
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset

24 

58801  25 
* Command 'notepad' requires proper nesting of begin/end and its proof 
26 
structure in the body: 'oops' is no longer supported here. Minor 

27 
INCOMPATIBILITY, use 'sorry' instead. 

28 

58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset

29 
* Outer syntax commands are managed authentically within the theory 
59569  30 
context, without implicit global state. Potential for accidental 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset

31 
INCOMPATIBILITY, make sure that required theories are really imported. 
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset

32 

59105  33 
* 'find_theorems': search patterns which are abstractions are 
59570  34 
schematically expanded before search. Search results match the naive 
59569  35 
expectation more closely, particularly wrt. abbreviations. 
59105  36 
INCOMPATIBILITY. 
37 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

38 

58524  39 
*** Prover IDE  Isabelle/Scala/jEdit *** 
40 

59308  41 
* Old graph browser (Java/AWT 1.0) is superseded by improved graphview 
42 
panel, which also includes PDF output. 

43 

59569  44 
* Improved folding mode "isabelle" based on Isar syntax. Alternatively, 
45 
the "sidekick" mode may be used for document structure. 

46 

47 
* Extended bracket matching based on Isar language structure. System 

48 
option jedit_structure_limit determines maximum number of lines to scan 

49 
in the buffer. 

58758  50 

58540  51 
* Support for BibTeX files: context menu, contextsensitive token 
52 
marker, SideKick parser. 

58524  53 

58551  54 
* Document antiquotation @{cite} provides formal markup, which is 
55 
interpreted semiformally based on .bib files that happen to be opened 

58592  56 
in the editor (hyperlinks, completion etc.). 
58551  57 

58785  58 
* Less waste of vertical space via negative line spacing (see Global 
59 
Options / Text Area). 

60 

58524  61 

58202  62 
*** Pure *** 
63 

59792  64 
* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" 
65 
etc.) allow an optional context of local variables ('for' declaration): 

66 
these variables become schematic in the instantiated theorem. This 

67 
behaviour is analogous to 'for' in attributes "where" and "of". 

68 

58202  69 
* Command "class_deps" takes optional sort arguments constraining 
70 
the search space. 

71 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset

72 
* Lexical separation of signed and unsigend numerals: categories "num" 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset

73 
and "float" are unsigend. INCOMPATIBILITY: subtle change in precedence 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset

74 
of numeral signs, particulary in expressions involving infix syntax like 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset

75 
"( 1) ^ n". 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset

76 

58421  77 
* Old inner token category "xnum" has been discontinued. Potential 
78 
INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" 

79 
token category instead. 

80 

58202  81 

57737  82 
*** HOL *** 
83 

59739  84 
* New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for 
85 
singlestep rewriting with subterm selection based on patterns. 

86 

59746
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59739
diff
changeset

87 
* The functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" 
59659
1ce77bca58f8
Removed the infix operator "choose" to allow HOLCF to build
paulson <lp15@cam.ac.uk>
parents:
59648
diff
changeset

88 
type, so in particular on "real" and "complex" uniformly. 
1ce77bca58f8
Removed the infix operator "choose" to allow HOLCF to build
paulson <lp15@cam.ac.uk>
parents:
59648
diff
changeset

89 
Minor INCOMPATIBILITY: type constraints may be needed. 
1ce77bca58f8
Removed the infix operator "choose" to allow HOLCF to build
paulson <lp15@cam.ac.uk>
parents:
59648
diff
changeset

90 

59751
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset

91 
* New library of properties of the complex transcendental functions sin, cos, tan, exp, 
59746
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59739
diff
changeset

92 
ported from HOL Light. 
ddae5727c5a9
new HOL Light material about exp, sin, cos
paulson <lp15@cam.ac.uk>
parents:
59739
diff
changeset

93 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59661
diff
changeset

94 
* The factorial function, "fact", now has type "nat => 'a" (of a sort that admits 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59661
diff
changeset

95 
numeric types including nat, int, real and complex. INCOMPATIBILITY: 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59661
diff
changeset

96 
an expression such as "fact 3 = 6" may require a type constraint, and the combination 
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59661
diff
changeset

97 
"real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary, 
59751
916c0f6c83e3
New material for complex sin, cos, tan, Ln, also some reorganisation
paulson <lp15@cam.ac.uk>
parents:
59746
diff
changeset

98 
then use "of_nat (fact k)" or "real_of_nat (fact k)". 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59661
diff
changeset

99 

59587
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59570
diff
changeset

100 
* removed functions "natfloor" and "natceiling", 
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59570
diff
changeset

101 
use "nat o floor" and "nat o ceiling" instead. 
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59570
diff
changeset

102 
A few of the lemmas have been retained and adapted: in their names 
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59570
diff
changeset

103 
"natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling". 
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59570
diff
changeset

104 

59557  105 
* Qualified some duplicated fact names required for boostrapping 
106 
the type class hierarchy: 

107 
ab_add_uminus_conv_diff ~> diff_conv_add_uminus 

108 
field_inverse_zero ~> inverse_zero 

109 
field_divide_inverse ~> divide_inverse 

110 
field_inverse ~> left_inverse 

111 
Minor INCOMPATIBILITY. 

112 

59555  113 
* Eliminated fact duplicates: 
114 
mult_less_imp_less_right ~> mult_right_less_imp_less 

115 
mult_less_imp_less_left ~> mult_left_less_imp_less 

116 
Minor INCOMPATIBILITY. 

117 

59536  118 
* Fact consolidation: even_less_0_iff is subsumed by 
119 
double_add_less_zero_iff_single_add_less_zero (simp by default anyway). 

120 

59569  121 
* Discontinued oldfashioned "codegen" tool. Code generation can always 
122 
be externally triggered using an appropriate ROOT file plus a 

123 
corresponding theory. Parametrization is possible using environment 

124 
variables, or ML snippets in the most extreme cases. Minor 

125 
INCOMPATIBILITY. 

59480  126 

58775
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58770
diff
changeset

127 
* Add NO_MATCHsimproc, allows to check for syntactic nonequality 
9cd64a66a765
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
hoelzl
parents:
58770
diff
changeset

128 

58649
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
58645
diff
changeset

129 
* Generalized and consolidated some theorems concerning divsibility: 
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
58645
diff
changeset

130 
dvd_reduce ~> dvd_add_triv_right_iff 
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
58645
diff
changeset

131 
dvd_plus_eq_right ~> dvd_add_right_iff 
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
58645
diff
changeset

132 
dvd_plus_eq_left ~> dvd_add_left_iff 
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
58645
diff
changeset

133 
Minor INCOMPATIBILITY. 
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
58645
diff
changeset

134 

58770  135 
* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" 
136 
and part of HOLMain. 

58645  137 
even_def ~> even_iff_mod_2_eq_zero 
58740  138 
INCOMPATIBILITY. 
58645  139 

58512
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset

140 
* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1 
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset

141 
Minor INCOMPATIBILITY. 
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset

142 

58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58775
diff
changeset

143 
* field_simps: Use NO_MATCHsimproc for distribution rules, to avoid 
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58775
diff
changeset

144 
nontermination in case of distributing a division. With this change 
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58775
diff
changeset

145 
field_simps is in some cases slightly less powerful, if it fails try 
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58775
diff
changeset

146 
to add algebra_simps, or use divide_simps. 
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58775
diff
changeset

147 
Minor INCOMPATIBILITY. 
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58775
diff
changeset

148 

58321  149 
* Bootstrap of listsum as special case of abstract product over lists. 
150 
Fact rename: 

151 
listsum_def ~> listsum.eq_foldr 

152 
INCOMPATIBILITY. 

153 

59569  154 
* Command and antiquotation "value" provide different evaluation slots 
155 
(again), where the previous strategy (nbe after ML) serves as default. 

58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
58067
diff
changeset

156 
Minor INCOMPATIBILITY. 
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
58067
diff
changeset

157 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

158 
* New (co)datatype package: 
58373  159 
 The 'datatype_new' command has been renamed 'datatype'. The old 
160 
command of that name is now called 'old_datatype' and is provided 

161 
by "~~/src/HOL/Library/Old_Datatype.thy". See 

162 
'isabelle doc datatypes' for information on porting. 

163 
INCOMPATIBILITY. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

164 
 Renamed theorems: 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

165 
disc_corec ~> corec_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

166 
disc_corec_iff ~> corec_disc_iff 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

167 
disc_exclude ~> distinct_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

168 
disc_exhaust ~> exhaust_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

169 
disc_map_iff ~> map_disc_iff 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

170 
sel_corec ~> corec_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

171 
sel_exhaust ~> exhaust_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

172 
sel_map ~> map_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

173 
sel_set ~> set_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

174 
sel_split ~> split_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

175 
sel_split_asm ~> split_sel_asm 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

176 
strong_coinduct ~> coinduct_strong 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

177 
weak_case_cong ~> case_cong_weak 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

178 
INCOMPATIBILITY. 
58192  179 
 The "no_code" option to "free_constructors", "datatype_new", and 
180 
"codatatype" has been renamed "plugins del: code". 

181 
INCOMPATIBILITY. 

58044  182 
 The rules "set_empty" have been removed. They are easy 
183 
consequences of other set rules "by auto". 

184 
INCOMPATIBILITY. 

185 
 The rule "set_cases" is now registered with the "[cases set]" 

57990  186 
attribute. This can influence the behavior of the "cases" proof 
187 
method when more than one case rule is applicable (e.g., an 

188 
assumption is of the form "w : set ws" and the method "cases w" 

189 
is invoked). The solution is to specify the case rule explicitly 

190 
(e.g. "cases w rule: widget.exhaust"). 

191 
INCOMPATIBILITY. 

59675  192 
 Renamed theories: 
193 
BNF_Comp ~> BNF_Composition 

194 
BNF_FP_Base ~> BNF_Fixpoint_Base 

195 
BNF_GFP ~> BNF_Greatest_Fixpoint 

196 
BNF_LFP ~> BNF_Least_Fixpoint 

197 
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions 

198 
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions 

199 
INCOMPATIBILITY. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

200 

6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

201 
* Old datatype package: 
58310  202 
 The old 'datatype' command has been renamed 'old_datatype', and 
58373  203 
'rep_datatype' has been renamed 'old_rep_datatype'. They are 
204 
provided by "~~/src/HOL/Library/Old_Datatype.thy". See 

58310  205 
'isabelle doc datatypes' for information on porting. 
58373  206 
INCOMPATIBILITY. 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

207 
 Renamed theorems: 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

208 
weak_case_cong ~> case_cong_weak 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

209 
INCOMPATIBILITY. 
58373  210 
 Renamed theory: 
211 
~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy 

212 
INCOMPATIBILITY. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

213 

58368  214 
* Product over lists via constant "listprod". 
215 

59039  216 
* Nitpick: 
217 
 Fixed soundness bug related to the strict and nonstrict subset 

218 
operations. 

219 

57737  220 
* Sledgehammer: 
59511  221 
 CVC4 is now included with Isabelle instead of CVC3 and run by 
222 
default. 

57737  223 
 Minimization is now always enabled by default. 
224 
Removed subcommand: 

225 
min 

59039  226 
 The proof reconstruction, both oneliners and Isar, has been 
227 
dramatically improved. 

228 
 Improved support for CVC4 and veriT. 

57737  229 

58062  230 
* Old and new SMT modules: 
58067  231 
 The old 'smt' method has been renamed 'old_smt' and moved to 
59569  232 
'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility, 
233 
until applications have been ported to use the new 'smt' method. For 

234 
the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must 

235 
be installed, and the environment variable "OLD_Z3_SOLVER" must 

236 
point to it. 

58062  237 
INCOMPATIBILITY. 
58067  238 
 The 'smt2' method has been renamed 'smt'. 
58060  239 
INCOMPATIBILITY. 
59569  240 
 New option 'smt_reconstruction_step_timeout' to limit the 
241 
reconstruction time of Z3 proof steps in the new 'smt' method. 

59216  242 
 New option 'smt_statistics' to display statistics of the new 'smt' 
243 
method, especially runtime statistics of Z3 proof reconstruction. 

58060  244 

58247
98d0f85d247f
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
nipkow
parents:
58202
diff
changeset

245 
* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc 
98d0f85d247f
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
nipkow
parents:
58202
diff
changeset

246 

58626  247 
* New infrastructure for compiling, running, evaluating and testing 
59569  248 
generated code in target languages in HOL/Library/Code_Test. See 
249 
HOL/Codegenerator_Test/Code_Test* for examples. 

58008  250 

58630  251 
* Library/Sum_of_Squares: simplified and improved "sos" method. Always 
252 
use local CSDP executable, which is much faster than the NEOS server. 

253 
The "sos_cert" functionality is invoked as "sos" with additional 

254 
argument. Minor INCOMPATIBILITY. 

255 

58990  256 
* HOLDecision_Procs: 
257 
 New counterexample generator quickcheck[approximation] for 

258 
inequalities of transcendental functions. 

259 
Uses hardware floating point arithmetic to randomly discover 

260 
potential counterexamples. Counterexamples are certified with the 

261 
'approximation' method. 

262 
See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for 

263 
examples. 

264 

59354  265 
* HOLProbability: Reworked measurability prover 
266 
 applies destructor rules repeatetly 

267 
 removed application splitting (replaced by destructor rule) 

59569  268 
 added congruence rules to rewrite measure spaces under the sets 
269 
projection 

270 

58630  271 

58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

272 
*** Document preparation *** 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

273 

59446  274 
* Discontinued obsolete option "document_graph": session_graph.pdf is 
59450  275 
produced unconditionally for HTML browser_info and PDFLaTeX document. 
59446  276 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

277 
* Document markup commands 'chapter', 'section', 'subsection', 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

278 
'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

279 
context, even before the initial 'theory' command. Obsolete proof 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

280 
commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

281 
discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw' 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

282 
instead. The old 'header' command is still retained for some time, but 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

283 
should be replaced by 'chapter', 'section' etc. (using "isabelle 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

284 
update_header"). Minor INCOMPATIBILITY. 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

285 

ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

286 
* Diagnostic commands and document markup commands within a proof do not 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

287 
affect the command tag for output. Thus commands like 'thm' are subject 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

288 
to proof document structure, and no longer "stick out" accidentally. 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

289 
Commands 'text' and 'txt' merely differ in the LaTeX style, not their 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58990
diff
changeset

290 
tags. Potential INCOMPATIBILITY in exotic situations. 
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58861
diff
changeset

291 

58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

292 
* Official support for "tt" style variants, via \isatt{...} or 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

293 
\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

294 
verbatim environment of LaTeX is no longer used. This allows @{ML} etc. 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

295 
as argument to other macros (such as footnotes). 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

296 

23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

297 
* Document antiquotation @{verbatim} prints ASCII text literally in "tt" 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

298 
style. 
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

299 

23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58708
diff
changeset

300 

58066  301 
*** ML *** 
302 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

303 
* The main operations to certify logical entities are Thm.ctyp_of and 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

304 
Thm.cterm_of with a local context; oldstyle global theory variants are 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

305 
available as Thm.global_ctyp_of and Thm.global_cterm_of. 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

306 
INCOMPATIBILITY. 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

307 

59582  308 
* Elementary operations in module Thm are no longer pervasive. 
309 
INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, 

310 
Thm.term_of etc. 

311 

59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59175
diff
changeset

312 
* Former combinators NAMED_CRITICAL and CRITICAL for central critical 
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59175
diff
changeset

313 
sections have been discontinued, in favour of the more elementary 
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59175
diff
changeset

314 
Multithreading.synchronized and its highlevel derivative 
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59175
diff
changeset

315 
Synchronized.var (which is usually sufficient in applications). Subtle 
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59175
diff
changeset

316 
INCOMPATIBILITY: synchronized access needs to be atomic and cannot be 
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59175
diff
changeset

317 
nested. 
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59175
diff
changeset

318 

59112  319 
* Cartouches within ML sources are turned into values of type 
320 
Input.source (with formal position information). 

321 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

322 
* Proper context for various elementary tactics: assume_tac, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59480
diff
changeset

323 
resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac, 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59480
diff
changeset

324 
compose_tac, Splitter.split_tac etc. INCOMPATIBILITY. 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58928
diff
changeset

325 

58066  326 
* Tactical PARALLEL_ALLGOALS is the most common way to refer to 
327 
PARALLEL_GOALS. 

328 

59057
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
59039
diff
changeset

329 
* Basic combinators map, fold, fold_map, split_list, apply are 
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
59039
diff
changeset

330 
available as parameterized antiquotations, e.g. @{map 4} for lists of 
5b649fb2f2e1
added ML antiquotation @{apply n} or @{apply n(k)};
wenzelm
parents:
59039
diff
changeset

331 
quadruples. 
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58630
diff
changeset

332 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59057
diff
changeset

333 
* Renamed "pairself" to "apply2", in accordance to @{apply 2}. 
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59057
diff
changeset

334 
INCOMPATIBILITY. 
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
59057
diff
changeset

335 

59139
e557a9ddee5f
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
wenzelm
parents:
59112
diff
changeset

336 
* Synchronized.value (ML) is actually synchronized (as in Scala): 
e557a9ddee5f
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
wenzelm
parents:
59112
diff
changeset

337 
subtle change of semantics with minimal potential for INCOMPATIBILITY. 
e557a9ddee5f
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
wenzelm
parents:
59112
diff
changeset

338 

59564
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset

339 
* Goal.prove_multi is superseded by the fully general Goal.prove_common, 
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset

340 
which also allows to specify a fork priority. 
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset

341 

58066  342 

58610  343 
*** System *** 
344 

58846  345 
* Support for Proof General and Isar TTY loop has been discontinued. 
346 
Minor INCOMPATIBILITY. 

58842  347 

59200  348 
* JVM system property "isabelle.threads" determines size of Scala thread 
349 
pool, like Isabelle system option "threads" for ML. 

350 

59201
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

351 
* JVM system property "isabelle.laf" determines the default Swing 
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

352 
lookandfeel, via internal class name or symbolic name as in the jEdit 
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

353 
menu Global Options / Appearance. 
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

354 

59175
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

355 
* System option "pretty_margin" is superseded by "thy_output_margin", 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

356 
which is also accessible via document antiquotation option "margin". 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

357 
Only the margin for document output may be changed, but not the global 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

358 
pretty printing: that is 76 for plain console output, and adapted 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

359 
dynamically in GUI frontends. Implementations of document 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

360 
antiquotations need to observe the margin explicitly according to 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

361 
Thy_Output.string_of_margin. Minor INCOMPATIBILITY. 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59139
diff
changeset

362 

58861
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58846
diff
changeset

363 
* Historical commandline terminator ";" is no longer accepted. Minor 
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58846
diff
changeset

364 
INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete 
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58846
diff
changeset

365 
semicolons from theory sources. 
5ff61774df11
commandline terminator ";" is no longer accepted;
wenzelm
parents:
58846
diff
changeset

366 

58610  367 
* The Isabelle tool "update_cartouches" changes theory files to use 
368 
cartouches instead of oldstyle {* verbatim *} or `alt_string` tokens. 

369 

370 

57695  371 

57452  372 
New in Isabelle2014 (August 2014) 
373 
 

54055  374 

54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

375 
*** General *** 
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

376 

57452  377 
* Support for official Standard ML within the Isabelle context. 
378 
Command 'SML_file' reads and evaluates the given Standard ML file. 

379 
Toplevel bindings are stored within the theory context; the initial 

380 
environment is restricted to the Standard ML implementation of 

381 
Poly/ML, without the addons of Isabelle/ML. Commands 'SML_import' 

382 
and 'SML_export' allow to exchange toplevel bindings between the two 

383 
separate environments. See also ~~/src/Tools/SML/Examples.thy for 

384 
some examples. 

56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56450
diff
changeset

385 

57504  386 
* Standard tactics and proof methods such as "clarsimp", "auto" and 
387 
"safe" now preserve equality hypotheses "x = expr" where x is a free 

388 
variable. Locale assumptions and chained facts containing "x" 

389 
continue to be useful. The new method "hypsubst_thin" and the 

390 
configuration option "hypsubst_thin" (within the attribute name space) 

391 
restore the previous behavior. INCOMPATIBILITY, especially where 

392 
induction is done after these methods or when the names of free and 

393 
bound variables clash. As first approximation, old proofs may be 

394 
repaired by "using [[hypsubst_thin = true]]" in the critical spot. 

395 

56232  396 
* More static checking of proof methods, which allows the system to 
397 
form a closure over the concrete syntax. Method arguments should be 

398 
processed in the original proof context as far as possible, before 

399 
operating on the goal state. In any case, the standard discipline for 

400 
subgoaladdressing needs to be observed: no subgoals or a subgoal 

401 
number that is out of range produces an empty result sequence, not an 

402 
exception. Potential INCOMPATIBILITY for nonconformant tactical 

403 
proof tools. 

404 

57452  405 
* Lexical syntax (inner and outer) supports text cartouches with 
406 
arbitrary nesting, and without escapes of quotes etc. The Prover IDE 

407 
supports input via ` (backquote). 

408 

409 
* The outer syntax categories "text" (for formal comments and document 

410 
markup commands) and "altstring" (for literal fact references) allow 

411 
cartouches as well, in addition to the traditional mix of quotations. 

412 

413 
* Syntax of document antiquotation @{rail} now uses \<newline> instead 

414 
of "\\", to avoid the optical illusion of escaped backslash within 

57491  415 
string token. General renovation of its syntax using text cartouches. 
57452  416 
Minor INCOMPATIBILITY. 
417 

418 
* Discontinued legacy_isub_isup, which was a temporary workaround for 

419 
Isabelle/ML in Isabelle20131. The prover process no longer accepts 

420 
old identifier syntax with \<^isub> or \<^isup>. Potential 

421 
INCOMPATIBILITY. 

422 

423 
* Document antiquotation @{url} produces markup for the given URL, 

424 
which results in an active hyperlink within the text. 

425 

426 
* Document antiquotation @{file_unchecked} is like @{file}, but does 

427 
not check existence within the filesystem. 

428 

429 
* Updated and extended manuals: codegen, datatypes, implementation, 

430 
isarref, jedit, system. 

57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

431 

54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

432 

54533  433 
*** Prover IDE  Isabelle/Scala/jEdit *** 
434 

57650  435 
* Improved Document panel: simplified interaction where every single 
57452  436 
mouse click (re)opens document via desktop environment or as jEdit 
437 
buffer. 

438 

439 
* Support for Navigator plugin (with toolbar buttons), with connection 

440 
to PIDE hyperlinks. 

441 

442 
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. 

443 
Open text buffers take precedence over copies within the filesystem. 

444 

445 
* Improved support for Isabelle/ML, with jEdit mode "isabelleml" for 

446 
auxiliary ML files. 

57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

447 

96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

448 
* Improved syntactic and semantic completion mechanism, with simple 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

449 
templates, completion language context, namespace completion, 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

450 
filename completion, spellchecker completion. 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

451 

96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

452 
* 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

453 
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

454 
keystrokes with slow / remote graphics displays. 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

455 

57833
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset

456 
* 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

457 
item, depending on Isabelle options. 
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset

458 

57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

459 
* 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

460 
selections, rectangular selections, rectangular selection as "tall 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

461 
caret". 
56342  462 

56580  463 
* Integrated spellchecker for document text, comments etc. with 
57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

464 
completion popup and contextmenu. 
56554  465 

56879
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset

466 
* More general "Query" panel supersedes "Find" panel, with GUI access 
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset

467 
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

468 
operations for the context. Minor incompatibility in keyboard 
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset

469 
shortcuts etc.: replace action isabellefind by isabellequery. 
56761  470 

56901  471 
* Search field for all output panels ("Output", "Query", "Info" etc.) 
472 
to highlight text via regular expression. 

473 

54881  474 
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle / 
475 
General") allows to specify additional print modes for the prover 

476 
process, without requiring oldfashioned commandline invocation of 

477 
"isabelle jedit m MODE". 

478 

56505  479 
* More support for remote files (e.g. http) using standard Java 
480 
networking operations instead of jEdit virtual filesystems. 

481 

57822  482 
* Empty editors buffers that are no longer required (e.g.\ via theory 
483 
imports) are automatically removed from the document model. 

484 

57869  485 
* Improved monitor panel. 
486 

56838  487 
* Improved Console/Scala plugin: more uniform scala.Console output, 
488 
more robust treatment of threads and interrupts. 

489 

56939  490 
* Improved management of dockable windows: clarified keyboard focus 
491 
and window placement wrt. main editor view; optional menu item to 

492 
"Detach" a copy where this makes sense. 

493 

57452  494 
* New Simplifier Trace panel provides an interactive view of the 
57591
8c095aef6769
clarified "simp_trace_new" and corresponding isarref section;
wenzelm
parents:
57532
diff
changeset

495 
simplification process, enabled by the "simp_trace_new" attribute 
57452  496 
within the context. 
497 

498 

55001  499 
*** Pure *** 
500 

57504  501 
* Lowlevel typeclass commands 'classes', 'classrel', 'arities' have 
502 
been discontinued to avoid the danger of nontrivial axiomatization 

503 
that is not immediately visible. INCOMPATIBILITY, use regular 

504 
'instance' command with proof. The required OFCLASS(...) theorem 

505 
might be postulated via 'axiomatization' beforehand, or the proof 

506 
finished trivially if the underlying class definition is made vacuous 

507 
(without any assumptions). See also Isabelle/ML operations 

508 
Axclass.class_axiomatization, Axclass.classrel_axiomatization, 

509 
Axclass.arity_axiomatization. 

510 

56245  511 
* Basic constants of Pure use more conventional names and are always 
512 
qualified. Rare INCOMPATIBILITY, but with potentially serious 

513 
consequences, notably for tools in Isabelle/ML. The following 

514 
renaming needs to be applied: 

515 

516 
== ~> Pure.eq 

517 
==> ~> Pure.imp 

518 
all ~> Pure.all 

519 
TYPE ~> Pure.type 

520 
dummy_pattern ~> Pure.dummy_pattern 

521 

522 
Systematic porting works by using the following theory setup on a 

523 
*previous* Isabelle version to introduce the new name accesses for the 

524 
old constants: 

525 

526 
setup {* 

527 
fn thy => thy 

528 
> Sign.root_path 

529 
> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "==" 

530 
> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>" 

531 
> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all" 

532 
> Sign.restore_naming thy 

533 
*} 

534 

535 
Thus ML antiquotations like @{const_name Pure.eq} may be used already. 

536 
Later the application is moved to the current Isabelle version, and 

537 
the auxiliary aliases are deleted. 

538 

55143
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

539 
* Attributes "where" and "of" allow an optional context of local 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

540 
variables ('for' declaration): these variables become schematic in the 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

541 
instantiated theorem. 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

542 

55152  543 
* Obsolete attribute "standard" has been discontinued (legacy since 
544 
Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context 

545 
where instantiations with schematic variables are intended (for 

546 
declaration commands like 'lemmas' or attributes like "of"). The 

547 
following temporary definition may help to port old applications: 

548 

549 
attribute_setup standard = 

550 
"Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))" 

551 

55001  552 
* More thorough check of proof context for goal statements and 
55006  553 
attributed fact expressions (concerning background theory, declared 
554 
hyps). Potential INCOMPATIBILITY, tools need to observe standard 

555 
context discipline. See also Assumption.add_assumes and the more 

556 
primitive Thm.assume_hyps. 

55001  557 

55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset

558 
* Inner syntax token language allows regular quoted strings "..." 
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset

559 
(only makes sense in practice, if outer syntax is delimited 
57452  560 
differently, e.g. via cartouches). 
561 

57504  562 
* Command 'print_term_bindings' supersedes 'print_binds' for clarity, 
563 
but the latter is retained some time as Proof General legacy. 

564 

57452  565 
* Code generator preprocessor: explicit control of simp tracing on a 
566 
perconstant basis. See attribute "code_preproc". 

57430
020cea57eaa4
tracing facilities for the code generator preprocessor
haftmann
parents:
57423
diff
changeset

567 

55001  568 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset

569 
*** HOL *** 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset

570 

57504  571 
* Code generator: enforce case of identifiers only for strict target 
572 
language requirements. INCOMPATIBILITY. 

573 

574 
* Code generator: explicit proof contexts in many ML interfaces. 

575 
INCOMPATIBILITY. 

576 

577 
* Code generator: minimize exported identifiers by default. Minor 

578 
INCOMPATIBILITY. 

579 

580 
* Code generation for SML and OCaml: dropped arcane "no_signatures" 

581 
option. Minor INCOMPATIBILITY. 

582 

583 
* "declare [[code abort: ...]]" replaces "code_abort ...". 

584 
INCOMPATIBILITY. 

585 

586 
* "declare [[code drop: ...]]" drops all code equations associated 

587 
with the given constants. 

588 

589 
* Code generations are provided for make, fields, extend and truncate 

590 
operations on records. 

57437  591 

57452  592 
* Command and antiquotation "value" are now hardcoded against nbe and 
593 
ML. Minor INCOMPATIBILITY. 

594 

57504  595 
* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY. 
596 

597 
* The symbol "\<newline>" may be used within char or string literals 

598 
to represent (Char Nibble0 NibbleA), i.e. ASCII newline. 

599 

600 
* Qualified String.implode and String.explode. INCOMPATIBILITY. 

56923  601 

57452  602 
* Simplifier: Enhanced solver of preconditions of rewrite rules can 
603 
now deal with conjunctions. For help with converting proofs, the old 

604 
behaviour of the simplifier can be restored like this: declare/using 

605 
[[simp_legacy_precond]]. This configuration option will disappear 

606 
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

607 

55139  608 
* Simproc "finite_Collect" is no longer enabled by default, due to 
609 
spurious crashes and other surprises. Potential INCOMPATIBILITY. 

610 

57452  611 
* Moved new (co)datatype package and its dependencies from session 
612 
"HOLBNF" to "HOL". The commands 'bnf', 'wrap_free_constructors', 

613 
'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now 

614 
part of theory "Main". 

615 

55098  616 
Theory renamings: 
617 
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) 

618 
Library/Wfrec.thy ~> Wfrec.thy 

619 
Library/Zorn.thy ~> Zorn.thy 

620 
Cardinals/Order_Relation.thy ~> Order_Relation.thy 

621 
Library/Order_Union.thy ~> Cardinals/Order_Union.thy 

622 
Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy 

623 
Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy 

624 
Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy 

625 
Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy 

626 
Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy 

627 
BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy 

628 
BNF/Basic_BNFs.thy ~> Basic_BNFs.thy 

629 
BNF/BNF_Comp.thy ~> BNF_Comp.thy 

630 
BNF/BNF_Def.thy ~> BNF_Def.thy 

631 
BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy 

632 
BNF/BNF_GFP.thy ~> BNF_GFP.thy 

633 
BNF/BNF_LFP.thy ~> BNF_LFP.thy 

634 
BNF/BNF_Util.thy ~> BNF_Util.thy 

635 
BNF/Coinduction.thy ~> Coinduction.thy 

636 
BNF/More_BNFs.thy ~> Library/More_BNFs.thy 

637 
BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy 

638 
BNF/Examples/* ~> BNF_Examples/* 

57452  639 

55098  640 
New theories: 
641 
Wellorder_Extension.thy (split from Zorn.thy) 

642 
Library/Cardinal_Notations.thy 

56942  643 
Library/BNF_Axomatization.thy 
55098  644 
BNF_Examples/Misc_Primcorec.thy 
645 
BNF_Examples/Stream_Processor.thy 

57452  646 

55519  647 
Discontinued theories: 
55098  648 
BNF/BNF.thy 
649 
BNF/Equiv_Relations_More.thy 

57452  650 

651 
INCOMPATIBILITY. 

55098  652 

56118
d3967fdc800a
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
blanchet
parents:
56076
diff
changeset

653 
* New (co)datatype package: 
57452  654 
 Command 'primcorec' is fully implemented. 
655 
 Command 'datatype_new' generates size functions ("size_xxx" and 

656 
"size") as required by 'fun'. 

657 
 BNFs are integrated with the Lifting tool and newstyle 

658 
(co)datatypes with Transfer. 

659 
 Renamed commands: 

55875  660 
datatype_new_compat ~> datatype_compat 
661 
primrec_new ~> primrec 

662 
wrap_free_constructors ~> free_constructors 

663 
INCOMPATIBILITY. 

57452  664 
 The generated constants "xxx_case" and "xxx_rec" have been renamed 
55875  665 
"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod"). 
666 
INCOMPATIBILITY. 

57452  667 
 The constant "xxx_(un)fold" and related theorems are no longer 
668 
generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually 

669 
using "prim(co)rec". 

55875  670 
INCOMPATIBILITY. 
57452  671 
 No discriminators are generated for nullary constructors by 
672 
default, eliminating the need for the odd "=:" syntax. 

57091  673 
INCOMPATIBILITY. 
57452  674 
 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

675 
"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

676 
"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

677 
INCOMPATIBILITY. 
55875  678 

55643  679 
* Old datatype package: 
57452  680 
 The generated theorems "xxx.cases" and "xxx.recs" have been 
681 
renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" > 

682 
"sum.case"). INCOMPATIBILITY. 

683 
 The generated constants "xxx_case", "xxx_rec", and "xxx_size" have 

684 
been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., 

685 
"prod_case" ~> "case_prod"). INCOMPATIBILITY. 

686 

687 
* The types "'a list" and "'a option", their set and map functions, 

688 
their relators, and their selectors are now produced using the new 

689 
BNFbased datatype package. 

690 

55519  691 
Renamed constants: 
692 
Option.set ~> set_option 

693 
Option.map ~> map_option 

55525  694 
option_rel ~> rel_option 
57452  695 

55519  696 
Renamed theorems: 
55585  697 
set_def ~> set_rec[abs_def] 
55519  698 
map_def ~> map_rec[abs_def] 
699 
Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") 

56652  700 
option.recs ~> option.rec 
55524
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55519
diff
changeset

701 
list_all2_def ~> list_all2_iff 
55585  702 
set.simps ~> set_simps (or the slightly different "list.set") 
55519  703 
map.simps ~> list.map 
704 
hd.simps ~> list.sel(1) 

705 
tl.simps ~> list.sel(23) 

706 
the.simps ~> option.sel 

57452  707 

708 
INCOMPATIBILITY. 

55519  709 

55933  710 
* The following map functions and relators have been renamed: 
55939  711 
sum_map ~> map_sum 
712 
map_pair ~> map_prod 

55944  713 
prod_rel ~> rel_prod 
55943  714 
sum_rel ~> rel_sum 
55945  715 
fun_rel ~> rel_fun 
55942  716 
set_rel ~> rel_set 
717 
filter_rel ~> rel_filter 

57452  718 
fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy") 
719 
cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy") 

720 
vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy") 

721 

722 
INCOMPATIBILITY. 

723 

57826  724 
* Lifting and Transfer: 
725 
 a type variable as a raw type is supported 

726 
 stronger reflexivity prover 

727 
 rep_eq is always generated by lift_definition 

57856  728 
 setup for Lifting/Transfer is now automated for BNFs 
57826  729 
+ holds for BNFs that do not contain a dead variable 
57856  730 
+ relator_eq, relator_mono, relator_distr, relator_domain, 
57826  731 
relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total, 
732 
right_unique, right_total, left_unique, left_total are proved 

733 
automatically 

734 
+ definition of a predicator is generated automatically 

735 
+ simplification rules for a predicator definition are proved 

736 
automatically for datatypes 

737 
 consolidation of the setup of Lifting/Transfer 

57856  738 
+ property that a relator preservers reflexivity is not needed any 
57826  739 
more 
740 
Minor INCOMPATIBILITY. 

57856  741 
+ left_total and left_unique rules are now transfer rules 
57826  742 
(reflexivity_rule attribute not needed anymore) 
743 
INCOMPATIBILITY. 

57856  744 
+ Domainp does not have to be a separate assumption in 
57826  745 
relator_domain theorems (=> more natural statement) 
746 
INCOMPATIBILITY. 

747 
 registration of code equations is more robust 

748 
Potential INCOMPATIBILITY. 

749 
 respectfulness proof obligation is preprocessed to a more readable 

750 
form 

751 
Potential INCOMPATIBILITY. 

752 
 eq_onp is always unfolded in respectfulness proof obligation 

753 
Potential INCOMPATIBILITY. 

57856  754 
 unregister lifting setup for Code_Numeral.integer and 
57826  755 
Code_Numeral.natural 
756 
Potential INCOMPATIBILITY. 

757 
 Lifting.invariant > eq_onp 

758 
INCOMPATIBILITY. 

57856  759 

57508  760 
* New internal SAT solver "cdclite" that produces models and proof 
761 
traces. This solver replaces the internal SAT solvers "enumerate" and 

762 
"dpll". Applications that explicitly used one of these two SAT 

763 
solvers should use "cdclite" instead. In addition, "cdclite" is now 

764 
the default SAT solver for the "sat" and "satx" proof methods and 

765 
corresponding tactics; the old default can be restored using "declare 

766 
[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. 

767 

768 
* SMT module: A new version of the SMT module, temporarily called 

769 
"SMT2", uses SMTLIB 2 and supports recent versions of Z3 (e.g., 

770 
4.3). The new proof method is called "smt2". CVC3 and CVC4 are also 

771 
supported as oracles. Yices is no longer supported, because no version 

772 
of the solver can handle both SMTLIB 2 and quantifiers. 

773 

774 
* Activation of Z3 now works via "z3_non_commercial" system option 

775 
(without requiring restart), instead of former settings variable 

776 
"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu 

777 
Plugin Options / Isabelle / General. 

778 

779 
* Sledgehammer: 

780 
 Z3 can now produce Isar proofs. 

781 
 MaSh overhaul: 

57532  782 
. New SMLbased learning algorithms eliminate the dependency on 
57508  783 
Python and increase performance and reliability. 
784 
. MaSh and MeSh are now used by default together with the 

785 
traditional MePo (MengPaulson) relevance filter. To disable 

786 
MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin 

787 
Options / Isabelle / General to "none". 

788 
 New option: 

789 
smt_proofs 

790 
 Renamed options: 

791 
isar_compress ~> compress 

792 
isar_try0 ~> try0 

793 

794 
INCOMPATIBILITY. 

795 

796 
* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. 

797 

798 
* Nitpick: 

799 
 Fixed soundness bug whereby mutually recursive datatypes could 

800 
take infinite values. 

801 
 Fixed soundness bug with lowlevel number functions such as 

802 
"Abs_Integ" and "Rep_Integ". 

803 
 Removed "std" option. 

804 
 Renamed "show_datatypes" to "show_types" and "hide_datatypes" to 

805 
"hide_types". 

806 

807 
* Metis: Removed legacy proof method 'metisFT'. Use 'metis 

808 
(full_types)' instead. INCOMPATIBILITY. 

809 

810 
* Try0: Added 'algebra' and 'meson' to the set of proof methods. 

811 

812 
* Adjustion of INF and SUP operations: 

813 
 Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. 

814 
 Consolidated theorem names containing INFI and SUPR: have INF and 

815 
SUP instead uniformly. 

816 
 More aggressive normalization of expressions involving INF and Inf 

817 
or SUP and Sup. 

818 
 INF_image and SUP_image do not unfold composition. 

819 
 Dropped facts INF_comp, SUP_comp. 

820 
 Default congruence rules strong_INF_cong and strong_SUP_cong, with 

821 
simplifier implication in premises. Generalize and replace former 

822 
INT_cong, SUP_cong 

823 

824 
INCOMPATIBILITY. 

825 

826 
* SUP and INF generalized to conditionally_complete_lattice. 

827 

828 
* Swapped orientation of facts image_comp and vimage_comp: 

829 

830 
image_compose ~> image_comp [symmetric] 

831 
image_comp ~> image_comp [symmetric] 

832 
vimage_compose ~> vimage_comp [symmetric] 

833 
vimage_comp ~> vimage_comp [symmetric] 

834 

835 
INCOMPATIBILITY. 

836 

57504  837 
* Theory reorganization: split of Big_Operators.thy into 
838 
Groups_Big.thy and Lattices_Big.thy. 

55098  839 

57418  840 
* Consolidated some facts about big group operators: 
841 

842 
setsum_0' ~> setsum.neutral 

843 
setsum_0 ~> setsum.neutral_const 

844 
setsum_addf ~> setsum.distrib 

845 
setsum_cartesian_product ~> setsum.cartesian_product 

846 
setsum_cases ~> setsum.If_cases 

847 
setsum_commute ~> setsum.commute 

848 
setsum_cong ~> setsum.cong 

849 
setsum_delta ~> setsum.delta 

850 
setsum_delta' ~> setsum.delta' 

851 
setsum_diff1' ~> setsum.remove 

852 
setsum_empty ~> setsum.empty 

853 
setsum_infinite ~> setsum.infinite 

854 
setsum_insert ~> setsum.insert 

855 
setsum_inter_restrict'' ~> setsum.inter_filter 

856 
setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left 

857 
setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right 

858 
setsum_mono_zero_left ~> setsum.mono_neutral_left 

859 
setsum_mono_zero_right ~> setsum.mono_neutral_right 

860 
setsum_reindex ~> setsum.reindex 

861 
setsum_reindex_cong ~> setsum.reindex_cong 

862 
setsum_reindex_nonzero ~> setsum.reindex_nontrivial 

863 
setsum_restrict_set ~> setsum.inter_restrict 

864 
setsum_Plus ~> setsum.Plus 

865 
setsum_setsum_restrict ~> setsum.commute_restrict 

866 
setsum_Sigma ~> setsum.Sigma 

867 
setsum_subset_diff ~> setsum.subset_diff 

868 
setsum_Un_disjoint ~> setsum.union_disjoint 

869 
setsum_UN_disjoint ~> setsum.UNION_disjoint 

870 
setsum_Un_Int ~> setsum.union_inter 

871 
setsum_Union_disjoint ~> setsum.Union_disjoint 

872 
setsum_UNION_zero ~> setsum.Union_comp 

873 
setsum_Un_zero ~> setsum.union_inter_neutral 

874 
strong_setprod_cong ~> setprod.strong_cong 

875 
strong_setsum_cong ~> setsum.strong_cong 

876 
setprod_1' ~> setprod.neutral 

877 
setprod_1 ~> setprod.neutral_const 

878 
setprod_cartesian_product ~> setprod.cartesian_product 

879 
setprod_cong ~> setprod.cong 

880 
setprod_delta ~> setprod.delta 

881 
setprod_delta' ~> setprod.delta' 

882 
setprod_empty ~> setprod.empty 

883 
setprod_infinite ~> setprod.infinite 

884 
setprod_insert ~> setprod.insert 

885 
setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left 

886 
setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right 

887 
setprod_mono_one_left ~> setprod.mono_neutral_left 

888 
setprod_mono_one_right ~> setprod.mono_neutral_right 

889 
setprod_reindex ~> setprod.reindex 

890 
setprod_reindex_cong ~> setprod.reindex_cong 

891 
setprod_reindex_nonzero ~> setprod.reindex_nontrivial 

892 
setprod_Sigma ~> setprod.Sigma 

893 
setprod_subset_diff ~> setprod.subset_diff 

894 
setprod_timesf ~> setprod.distrib 

895 
setprod_Un2 ~> setprod.union_diff2 

896 
setprod_Un_disjoint ~> setprod.union_disjoint 

897 
setprod_UN_disjoint ~> setprod.UNION_disjoint 

898 
setprod_Un_Int ~> setprod.union_inter 

899 
setprod_Union_disjoint ~> setprod.Union_disjoint 

900 
setprod_Un_one ~> setprod.union_inter_neutral 

901 

902 
Dropped setsum_cong2 (simple variant of setsum.cong). 

903 
Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict) 

904 
Dropped setsum_reindex_id, setprod_reindex_id 

905 
(simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]). 

906 

57452  907 
INCOMPATIBILITY. 
908 

54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

909 
* Abolished slightly odd global lattice interpretation for min/max. 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

910 

57452  911 
Fact consolidations: 
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

912 
min_max.inf_assoc ~> min.assoc 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

913 
min_max.inf_commute ~> min.commute 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

914 
min_max.inf_left_commute ~> min.left_commute 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

915 
min_max.inf_idem ~> min.idem 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

916 
min_max.inf_left_idem ~> min.left_idem 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

917 
min_max.inf_right_idem ~> min.right_idem 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

918 
min_max.sup_assoc ~> max.assoc 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

919 
min_max.sup_commute ~> max.commute 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

920 
min_max.sup_left_commute ~> max.left_commute 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

921 
min_max.sup_idem ~> max.idem 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

922 
min_max.sup_left_idem ~> max.left_idem 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

923 
min_max.sup_inf_distrib1 ~> max_min_distrib2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

924 
min_max.sup_inf_distrib2 ~> max_min_distrib1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

925 
min_max.inf_sup_distrib1 ~> min_max_distrib2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

926 
min_max.inf_sup_distrib2 ~> min_max_distrib1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

927 
min_max.distrib ~> min_max_distribs 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

928 
min_max.inf_absorb1 ~> min.absorb1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

929 
min_max.inf_absorb2 ~> min.absorb2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

930 
min_max.sup_absorb1 ~> max.absorb1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

931 
min_max.sup_absorb2 ~> max.absorb2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

932 
min_max.le_iff_inf ~> min.absorb_iff1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

933 
min_max.le_iff_sup ~> max.absorb_iff2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

934 
min_max.inf_le1 ~> min.cobounded1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

935 
min_max.inf_le2 ~> min.cobounded2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

936 
le_maxI1, min_max.sup_ge1 ~> max.cobounded1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

937 
le_maxI2, min_max.sup_ge2 ~> max.cobounded2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

938 
min_max.le_infI1 ~> min.coboundedI1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

939 
min_max.le_infI2 ~> min.coboundedI2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

940 
min_max.le_supI1 ~> max.coboundedI1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

941 
min_max.le_supI2 ~> max.coboundedI2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

942 
min_max.less_infI1 ~> min.strict_coboundedI1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

943 
min_max.less_infI2 ~> min.strict_coboundedI2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

944 
min_max.less_supI1 ~> max.strict_coboundedI1 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

945 
min_max.less_supI2 ~> max.strict_coboundedI2 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

946 
min_max.inf_mono ~> min.mono 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

947 
min_max.sup_mono ~> max.mono 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

948 
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

949 
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

950 
min_max.le_inf_iff ~> min.bounded_iff 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

951 
min_max.le_sup_iff ~> max.bounded_iff 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

952 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

953 
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

954 
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

955 
max.left_commute, max.left_idem directly. 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

956 

57452  957 
For min_max.inf_sup_ord, prefer (one of) min.cobounded1, 
958 
min.cobounded2, max.cobounded1m max.cobounded2 directly. 

54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

959 

56807  960 
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

961 

58604
13dfea1621b2
improved spelling of formal INCOMPATIBILITY in historic versions (!)  to avoid adhoc word completion multiply such lapses;
wenzelm
parents:
58592
diff
changeset

962 
INCOMPATIBILITY. 
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54850
diff
changeset

963 

57452  964 
* Theorem disambiguation Inf_le_Sup (on finite sets) ~> 
965 
Inf_fin_le_Sup_fin. INCOMPATIBILITY. 

54745  966 

54295  967 
* Qualified constant names Wellfounded.acc, Wellfounded.accp. 
968 
INCOMPATIBILITY. 

969 

54228  970 
* Fact generalization and consolidation: 
971 
neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 

57452  972 

973 
INCOMPATIBILITY. 

974 

975 
* Purely algebraic definition of even. Fact generalization and 

976 
consolidation: 

54228  977 
nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd 
978 
even_zero_(natint) ~> even_zero 

57452  979 

54228  980 
INCOMPATIBILITY. 
54055  981 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54449
diff
changeset

982 
* Abolished neg_numeral. 
57452  983 
 Canonical representation for minus one is " 1". 
984 
 Canonical representation for other negative numbers is " (numeral _)". 

985 
 When devising rule sets for number calculation, consider the 

54587  986 
following canonical cases: 0, 1, numeral _,  1,  numeral _. 
57452  987 
 HOLogic.dest_number also recognizes numerals in noncanonical forms 
54893
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset

988 
like "numeral One", " numeral One", " 0" and even " ...  _". 
57452  989 
 Syntax for negative numerals is mere input syntax. 
990 

56964  991 
INCOMPATIBILITY. 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54449
diff
changeset

992 

57517  993 
* Reduced name variants for rules on associativity and commutativity: 
994 

995 
add_assoc ~> add.assoc 

996 
add_commute ~> add.commute 

997 
add_left_commute ~> add.left_commute 

998 
mult_assoc ~> mult.assoc 

999 
mult_commute ~> mult.commute 

1000 
mult_left_commute ~> mult.left_commute 

1001 
nat_add_assoc ~> add.assoc 

1002 
nat_add_commute ~> add.commute 

1003 
nat_add_left_commute ~> add.left_commute 

1004 
nat_mult_assoc ~> mult.assoc 

1005 
nat_mult_commute ~> mult.commute 

1006 
eq_assoc ~> iff_assoc 

1007 
eq_left_commute ~> iff_left_commute 

1008 

1009 
INCOMPATIBILITY. 

1010 

57650  1011 
* Fact collections add_ac and mult_ac are considered oldfashioned. 
57637
eeb2d50ec71f
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
wenzelm
parents:
57591
diff
changeset

1012 
Prefer ac_simps instead, or specify rules 
eeb2d50ec71f
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
wenzelm
parents:
57591
diff
changeset

1013 
(addmult).(assoccommuteleft_commute) individually. 
57517  1014 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1015 
* Elimination of fact duplicates: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1016 
equals_zero_I ~> minus_unique 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1017 
diff_eq_0_iff_eq ~> right_minus_eq 
54588  1018 
nat_infinite ~> infinite_UNIV_nat 
1019 
int_infinite ~> infinite_UNIV_int 

57452  1020 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1021 
INCOMPATIBILITY. 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1022 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1023 
* Fact name consolidation: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1024 
diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus 
54250  1025 
minus_le_self_iff ~> neg_less_eq_nonneg 
1026 
le_minus_self_iff ~> less_eq_neg_nonpos 

1027 
neg_less_nonneg ~> neg_less_pos 

1028 
less_minus_self_iff ~> less_neg_neg [simp] 

57452  1029 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1030 
INCOMPATIBILITY. 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1031 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1032 
* More simplification rules on unary and binary minus: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1033 
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

1034 
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

1035 
add_minus_cancel, diff_add_cancel, le_add_same_cancel1, 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1036 
le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2, 
57452  1037 
minus_add_cancel, uminus_add_conv_diff. These correspondingly have 
1038 
been taken away from fact collections algebra_simps and field_simps. 

1039 
INCOMPATIBILITY. 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1040 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1041 
To restore proofs, the following patterns are helpful: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1042 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1043 
a) Arbitrary failing proof not involving "diff_def": 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1044 
Consider simplification with algebra_simps or field_simps. 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1045 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1046 
b) Lifting rules from addition to subtraction: 
54893
4061ec8adb1c
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8Isabelle in Isabelle/jEdit);
wenzelm
parents:
54890
diff
changeset

1047 
Try with "using <rule for addition> of [... " _" ...]" by simp". 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1048 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1049 
c) Simplification with "diff_def": just drop "diff_def". 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1050 
Consider simplification with algebra_simps or field_simps; 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1051 
or the brute way with 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54228
diff
changeset

1052 
"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

1053 

57452  1054 
* Introduce bdd_above and bdd_below in theory 
1055 
Conditionally_Complete_Lattices, use them instead of explicitly 

1056 
stating boundedness of sets. 

1057 

1058 
* ccpo.admissible quantifies only over nonempty chains to allow more 

1059 
syntaxdirected proof rules; the case of the empty chain shows up as 

1060 
additional case in fixpoint induction proofs. INCOMPATIBILITY. 

54264  1061 

56214  1062 
* Removed and renamed theorems in Series: 
1063 
summable_le ~> suminf_le 

1064 
suminf_le ~> suminf_le_const 

1065 
series_pos_le ~> setsum_le_suminf 

1066 
series_pos_less ~> setsum_less_suminf 

1067 
suminf_ge_zero ~> suminf_nonneg 

1068 
suminf_gt_zero ~> suminf_pos 

1069 
suminf_gt_zero_iff ~> suminf_pos_iff 

1070 
summable_sumr_LIMSEQ_suminf ~> summable_LIMSEQ 

1071 
suminf_0_le ~> suminf_nonneg [rotate] 

1072 
pos_summable ~> summableI_nonneg_bounded 

1073 
ratio_test ~> summable_ratio_test 

1074 

1075 
removed series_zero, replaced by sums_finite 

1076 

1077 
removed auxiliary lemmas: 

57452  1078 

56214  1079 
sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group, 
57452  1080 
half, le_Suc_ex_iff, lemma_realpow_diff_sumr, 
1081 
real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2, 

1082 
sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero, 

1083 
summable_convergent_sumr_iff, sumr_diff_mult_const 

1084 

56214  1085 
INCOMPATIBILITY. 
1086 

1087 
* Replace (F)DERIV syntax by has_derivative: 

1088 
 "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'" 

1089 

1090 
 "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'" 

1091 

1092 
 "f differentiable at x within s" replaces "_ differentiable _ in _" syntax 

1093 

1094 
 removed constant isDiff 

1095 

57452  1096 
 "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as 
1097 
input syntax. 

1098 

1099 
 "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed. 

56214  1100 

1101 
 Renamed FDERIV_... lemmas to has_derivative_... 

1102 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

1103 
 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

1104 

0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

1105 
 removed DERIV_intros, has_derivative_eq_intros 
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

1106 

57452  1107 
 introduced derivative_intros and deriative_eq_intros which 
1108 
includes now rules for DERIV, has_derivative and 

1109 
has_vector_derivative. 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

1110 

56214  1111 
 Other renamings: 
1112 
differentiable_def ~> real_differentiable_def 

1113 
differentiableE ~> real_differentiableE 

1114 
fderiv_def ~> has_derivative_at 

1115 
field_fderiv_def ~> field_has_derivative_at 

1116 
isDiff_der ~> differentiable_def 

1117 
deriv_fderiv ~> has_field_derivative_def 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56371
diff
changeset

1118 
deriv_def ~> DERIV_def 
57452  1119 

1120 
INCOMPATIBILITY. 

1121 

1122 
* Include more theorems in continuous_intros. Remove the 

1123 
continuous_on_intros, isCont_intros collections, these facts are now 

1124 
in continuous_intros. 

1125 

1126 
* Theorems about complex numbers are now stated only using Re and Im, 

1127 
the Complex constructor is not used anymore. It is possible to use 

1128 
primcorec to defined the behaviour of a complexvalued function. 

1129 

1130 
Removed theorems about the Complex constructor from the simpset, they 

1131 
are available as the lemma collection legacy_Complex_simps. This 

1132 
especially removes 

1133 

56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1134 
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

1135 

57452  1136 
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

1137 
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

1138 

57452  1139 
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

1140 

48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1141 
Renamings: 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1142 
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

1143 
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

1144 
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

1145 
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

1146 
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

1147 
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

1148 
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

1149 
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

1150 
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

1151 
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

1152 
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

1153 
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

1154 

48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1155 
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

1156 
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

1157 
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

1158 

48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1159 
Removed theorems: 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1160 
complex_zero_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1161 
complex_add_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1162 
complex_minus_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1163 
complex_diff_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1164 
complex_one_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1165 
complex_mult_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1166 
complex_inverse_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1167 
complex_scaleR_def 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56879
diff
changeset

1168 

57452  1169 
INCOMPATIBILITY. 
1170 

57504  1171 
* Theory Lubs moved HOL image to HOLLibrary. It is replaced by 
1172 
Conditionally_Complete_Lattices. INCOMPATIBILITY. 

1173 

1174 
* HOLLibrary: new theory src/HOL/Library/Tree.thy. 

1175 

1176 
* HOLLibrary: removed theory src/HOL/Library/Kleene_Algebra.thy; it 

1177 
is subsumed by session Kleene_Algebra in AFP. 

1178 

57856  1179 
* HOLLibrary / theory RBT: various constants and facts are hidden; 
1180 
lifting setup is unregistered. INCOMPATIBILITY. 

57826  1181 

57504  1182 
* HOLCardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. 
1183 

1184 
* HOLWord: bit representations prefer type bool over type bit. 

1185 
INCOMPATIBILITY. 

1186 

1187 
* HOLWord: 

1188 
 Abandoned fact collection "word_arith_alts", which is a duplicate 

1189 
of "word_arith_wis". 

1190 
 Dropped first (duplicated) element in fact collections 

1191 
"sint_word_ariths", "word_arith_alts", "uint_word_ariths", 

1192 
"uint_word_arith_bintrs". 

1193 

1194 
* HOLNumber_Theory: 

1195 
 consolidated the proofs of the binomial theorem 

1196 
 the function fib is again of type nat => nat and not overloaded 

1197 
 no more references to Old_Number_Theory in the HOL libraries 

1198 
(except the AFP) 

1199 

1200 
INCOMPATIBILITY. 

1201 

54787  1202 
* HOLMultivariate_Analysis: 
57452  1203 
 Type class ordered_real_vector for ordered vector spaces. 
1204 
 New theory Complex_Basic_Analysis defining complex derivatives, 

57253  1205 
holomorphic functions, etc., ported from HOL Light's canal.ml. 
57452  1206 
 Changed order of ordered_euclidean_space to be compatible with 
54787  1207 
pointwise ordering on products. Therefore instance of 
1208 
conditionally_complete_lattice and ordered_real_vector. 

1209 
INCOMPATIBILITY: use box instead of greaterThanLessThan or 

57452  1210 
explicit setcomprehensions with eucl_less for other (half)open 
54787  1211 
intervals. 
57476  1212 
 removed dependencies on type class ordered_euclidean_space with 
1213 
introduction of "cbox" on euclidean_space 

1214 
 renamed theorems: 

1215 
interval ~> box 

1216 
mem_interval ~> mem_box 

1217 
interval_eq_empty ~> box_eq_empty 

1218 
interval_ne_empty ~> box_ne_empty 

1219 
interval_sing(1) ~> cbox_sing 

1220 
interval_sing(2) ~> box_sing 

1221 
subset_interval_imp ~> subset_box_imp 

1222 
subset_interval ~> subset_box 

1223 
open_interval ~> open_box 

1224 
closed_interval ~> closed_cbox 

1225 
interior_closed_interval ~> interior_cbox 

1226 
bounded_closed_interval ~> bounded_cbox 

1227 
compact_interval ~> compact_cbox 

1228 
bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric 

1229 
bounded_subset_closed_interval ~> bounded_subset_cbox 

1230 
mem_interval_componentwiseI ~> mem_box_componentwiseI 

1231 
convex_box ~> convex_prod 

1232 
rel_interior_real_interval ~> rel_interior_real_box 

1233 
convex_interval ~> convex_box 

1234 
convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox 

1235 
frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox 

1236 
content_closed_interval' ~> content_cbox' 

1237 
elementary_subset_interval ~> elementary_subset_box 

1238 
diameter_closed_interval ~> diameter_cbox 

1239 
frontier_closed_interval ~> frontier_cbox 

1240 
frontier_open_interval ~> frontier_box 

1241 
bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric 

1242 
closure_open_interval ~> closure_box 

1243 
open_closed_interval_convex ~> open_cbox_convex 

1244 
open_interval_midpoint ~> box_midpoint 

1245 
content_image_affinity_interval ~> content_image_affinity_cbox 

1246 
is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval 

1247 
bounded_interval ~> bounded_closed_interval + bounded_boxes 

1248 

1249 
 respective theorems for intervals over the reals: 

1250 
content_closed_interval + content_cbox 

1251 
has_integral + has_integral_real 

1252 
fine_division_exists + fine_division_exists_real 

1253 
has_integral_null + has_integral_null_real 

1254 
tagged_division_union_interval + tagged_division_union_interval_real 

1255 
has_integral_const + has_integral_const_real 

1256 
integral_const + integral_const_real 

1257 
has_integral_bound + has_integral_bound_real 

1258 
integrable_continuous + integrable_continuous_real 

1259 
integrable_subinterval + integrable_subinterval_real 

1260 
has_integral_reflect_lemma + has_integral_reflect_lemma_real 

1261 
integrable_reflect + integrable_reflect_real 

1262 
integral_reflect + integral_reflect_real 

1263 
image_affinity_interval + image_affinity_cbox 

1264 
image_smult_interval + image_smult_cbox 

1265 
integrable_const + integrable_const_ivl 

1266 
integrable_on_subinterval + integrable_on_subcbox 

1267 

56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset

1268 
 renamed theorems: 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset

1269 
derivative_linear ~> has_derivative_bounded_linear 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset

1270 
derivative_is_linear ~> has_derivative_linear 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset

1271 
bounded_linear_imp_linear ~> bounded_linear.linear 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56342
diff
changeset

1272 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1273 
* HOLProbability: 
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1274 
 Renamed positive_integral to nn_integral: 
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1275 

58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1276 
. 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

1277 
positive_integral_positive ~> nn_integral_nonneg 
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1278 

58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1279 
. 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

1280 

57452  1281 
 replaced the Lebesgue integral on real numbers by the more general 
1282 
Bochner integral for functions into a realnormed vector space. 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1283 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1284 
integral_zero ~> integral_zero / integrable_zero 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1285 
integral_minus ~> integral_minus / integrable_minus 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1286 
integral_add ~> integral_add / integrable_add 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1287 
integral_diff ~> integral_diff / integrable_diff 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1288 
integral_setsum ~> integral_setsum / integrable_setsum 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1289 
integral_multc ~> integral_mult_left / integrable_mult_left 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1290 
integral_cmult ~> integral_mult_right / integrable_mult_right 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1291 
integral_triangle_inequality~> integral_norm_bound 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1292 
integrable_nonneg ~> integrableI_nonneg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1293 
integral_positive ~> integral_nonneg_AE 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1294 
integrable_abs_iff ~> integrable_abs_cancel 
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1295 
positive_integral_lim_INF ~> nn_integral_liminf 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1296 
lebesgue_real_affine ~> lborel_real_affine 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1297 
borel_integral_has_integral ~> has_integral_lebesgue_integral 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1298 
integral_indicator ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1299 
integral_real_indicator / integrable_real_indicator 
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1300 
positive_integral_fst ~> nn_integral_fst' 
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1301 
positive_integral_fst_measurable ~> nn_integral_fst 
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1302 
positive_integral_snd_measurable ~> nn_integral_snd 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1303 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1304 
integrable_fst_measurable ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1305 
integral_fst / integrable_fst / AE_integrable_fst 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1306 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1307 
integrable_snd_measurable ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1308 
integral_snd / integrable_snd / AE_integrable_snd 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1309 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1310 
integral_monotone_convergence ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1311 
integral_monotone_convergence / integrable_monotone_convergence 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1312 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1313 
integral_monotone_convergence_at_top ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1314 
integral_monotone_convergence_at_top / 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1315 
integrable_monotone_convergence_at_top 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1316 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1317 
has_integral_iff_positive_integral_lebesgue ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1318 
has_integral_iff_has_bochner_integral_lebesgue_nonneg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1319 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1320 
lebesgue_integral_has_integral ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1321 
has_integral_integrable_lebesgue_nonneg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1322 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1323 
positive_integral_lebesgue_has_integral ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1324 
integral_has_integral_lebesgue_nonneg / 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1325 
integrable_has_integral_lebesgue_nonneg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1326 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1327 
lebesgue_integral_real_affine ~> 
57825
58f46c678352
better ordering of positive_integral renaming to nn_integral in NEWS
hoelzl
parents:
57822
diff
changeset

1328 
nn_integral_real_affine 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1329 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1330 
has_integral_iff_positive_integral_lborel ~> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1331 
integral_has_integral_nonneg / integrable_has_integral_nonneg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1332 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1333 
The following theorems where removed: 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1334 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1335 
lebesgue_integral_nonneg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1336 
lebesgue_integral_uminus 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1337 
lebesgue_integral_cmult 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1338 
lebesgue_integral_multc 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1339 
lebesgue_integral_cmult_nonneg 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1340 
integral_cmul_indicator 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56964
diff
changeset

1341 
integral_real 
54672
748778ac0ab8
relocate NEWS to postrelease version (cf. 7a14f831d02d);
wenzelm
parents:
54671
diff
changeset

1342 

57452  1343 
 Formalized properties about exponentially, Erlang, and normal 
1344 
distributed random variables. 

1345 

57504  1346 
* HOLDecision_Procs: Separate command 'approximate' for approximative 
1347 
computation in src/HOL/Decision_Procs/Approximation. Minor 

1348 
INCOMPATIBILITY. 

57452  1349 

57112
70395c65c0e3
removed Kleene_Algebra because of superior AFP entry; authors agreed
nipkow
parents:
57094
diff
changeset

1350 

55622
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset

1351 
*** Scala *** 
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset

1352 

ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset

1353 
* 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

1354 
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

1355 
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

1356 
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

1357 
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

1358 

57452  1359 
* Substantial reworking of internal PIDE protocol communication 
1360 
channels. INCOMPATIBILITY. 

1361 

55622
ce575c2212fc
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents:
55585
diff
changeset

1362 

54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset

1363 
*** ML *** 
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset

1364 

57504  1365 
* Subtle change of semantics of Thm.eq_thm: theory stamps are not 
1366 
compared (according to Thm.thm_ord), but assumed to be covered by the 

1367 
current background theory. Thus equivalent data produced in different 

1368 
branches of the theory graph usually coincides (e.g. relevant for 

1369 
theory merge). Note that the softer Thm.eq_thm_prop is often more 

1370 
appropriate than Thm.eq_thm. 

1371 

1372 
* Proper context for basic Simplifier operations: rewrite_rule, 

1373 
rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to 

1374 
pass runtime Proof.context (and ensure that the simplified entity 

1375 
actually belongs to it). 

1376 

1377 
* Proper context discipline for read_instantiate and instantiate_tac: 

1378 
variables that are meant to become schematic need to be given as 

1379 
fixed, and are generalized by the explicit context of local variables. 

1380 
This corresponds to Isar attributes "where" and "of" with 'for' 

1381 
declaration. INCOMPATIBILITY, also due to potential change of indices 

1382 
of schematic variables. 

1383 

56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56285
diff
changeset

1384 
* 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

1385 
structure Runtime. Minor INCOMPATIBILITY. 
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56285
diff
changeset

1386 

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

1387 
* Discontinued old Toplevel.debug in favour of system option 
57452  1388 
"ML_exception_trace", which may be also declared within the context 
1389 
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

1390 

56281  1391 
* Renamed configuration option "ML_trace" to "ML_source_trace". Minor 
1392 
INCOMPATIBILITY. 

1393 

1394 
* Configuration option "ML_print_depth" controls the prettyprinting 

1395 
depth of the ML compiler within the context. The old print_depth in 

56285  1396 
ML is still available as default_print_depth, but rarely used. Minor 
1397 
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

1398 

54449
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset

1399 
* Toplevel function "use" refers to raw ML bootstrap environment, 
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset

1400 
without Isar context nor antiquotations. Potential INCOMPATIBILITY. 
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset

1401 
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

1402 
formal context. 
f3cfe882f9af
toplevel function "use" refers to raw ML bootstrap environment;
wenzelm
parents:
54384
diff
changeset

1403 

56205  1404 
* Simplified programming interface to define ML antiquotations, see 
1405 
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

1406 

56071  1407 
* ML antiquotation @{here} refers to its source position, which is 
1408 
occasionally useful for experimentation and diagnostic purposes. 

1409 

56135  1410 
* ML antiquotation @{path} produces a Path.T value, similarly to 
1411 
Path.explode, but with compiletime check against the filesystem and 

1412 
some PIDE markup. Note that unlike theory source, ML does not have a 

1413 
welldefined master directory, so an absolute symbolic path 

1414 
specification is usually required, e.g. "~~/src/HOL". 