author  wenzelm 
Fri, 24 Sep 2021 13:40:14 +0200  
changeset 74360  9e71155e3666 
parent 74349  4974c3697fee 
permissions  rwrr 
57491  1 
Isabelle NEWS  history of userrelevant changes 
2 
================================================= 

2553  3 

62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
62111
diff
changeset

4 
(Note: Isabelle/jEdit shows a treeview of the NEWS file in Sidekick.) 
60006  5 

73272  6 

7 
New in this Isabelle version 

8 
 

9 

73387  10 
*** General *** 
11 

74335  12 
* Commands 'syntax' and 'no_syntax' now work in a local theory context, 
13 
but there is no proper way to refer to local entities  in contrast to 

14 
'notation' and 'no_notation'. Local syntax works well with 'bundle', 

15 
e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of 

16 
Isabelle/HOL. 

17 

74156  18 
* Configuration option "show_results" controls output of final results 
19 
in commands like 'definition' or 'theorem'. Output is normally enabled 

20 
in interactive mode, but it could occasionally cause unnecessary 

21 
slowdown. It can be disabled like this: 

22 

74349  23 
context notes [[show_results = false]] 
74156  24 
begin 
25 
definition "test = True" 

26 
theorem test by (simp add: test_def) 

27 
end 

28 

73387  29 
* Timeouts for Isabelle/ML tools are subject to system option 
30 
"timeout_scale"  this already used for the overall session build 

31 
process before, and allows to adapt to slow machines. The underlying 

32 
Timeout.apply in Isabelle/ML treats an original timeout specification 0 

33 
as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY 

34 
in boundary cases. 

35 

73436
e92f2e44e4d8
removed spurious references to perl / libwwwperl;
wenzelm
parents:
73411
diff
changeset

36 
* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now 
e92f2e44e4d8
removed spurious references to perl / libwwwperl;
wenzelm
parents:
73411
diff
changeset

37 
managed via Isabelle/Scala instead of perl; the dependency on 
e92f2e44e4d8
removed spurious references to perl / libwwwperl;
wenzelm
parents:
73411
diff
changeset

38 
libwwwperl has been eliminated (notably on Linux). Rare 
e92f2e44e4d8
removed spurious references to perl / libwwwperl;
wenzelm
parents:
73411
diff
changeset

39 
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties 
e92f2e44e4d8
removed spurious references to perl / libwwwperl;
wenzelm
parents:
73411
diff
changeset

40 
https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/docfiles/netproperties.html 
e92f2e44e4d8
removed spurious references to perl / libwwwperl;
wenzelm
parents:
73411
diff
changeset

41 

73446
d1c4c2395650
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelleutp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents:
73436
diff
changeset

42 
* More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). 
d1c4c2395650
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelleutp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents:
73436
diff
changeset

43 
See also the group "Z Notation" in the Symbols dockable of 
d1c4c2395650
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelleutp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents:
73436
diff
changeset

44 
Isabelle/jEdit. 
d1c4c2395650
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelleutp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents:
73436
diff
changeset

45 

73387  46 

73616  47 
*** Isabelle/jEdit Prover IDE *** 
48 

49 
* More robust 'proof' outline for method "induct": support nested cases. 

50 

73876  51 
* Support for builtin font substitution of jEdit text area. 
52 

74003  53 
* The main plugin for Isabelle/jEdit can be deactivated and reactivated 
54 
as documented  was broken at least since Isabelle2018. 

55 

73616  56 

73404  57 
*** Document preparation *** 
58 

73830  59 
* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX package 
73828  60 
"pifont"). 
61 

73830  62 
* Highquality blackboardbold symbols from font "txmia" (LaTeX package 
73828  63 
"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>. 
64 

73771  65 
* Document antiquotations for ML text have been refined: "def" and "ref" 
66 
variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def} 

67 
(bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit 

68 
type arguments for constructors (only relevant for index), e.g. 

69 
@{ML_type \<open>'a list\<close>} vs. @{ML_type 'a \<open>list\<close>}; @{ML_op} has been renamed 

70 
to @{ML_infix}. Minor INCOMPATIBILITY concerning name and syntax. 

71 

73723  72 
* Option "document_logo" determines if an instance of the Isabelle logo 
73 
should be created in the document output directory. The given string 

74 
specifies the name of the logo variant, while "_" (underscore) refers to 

75 
the unnamed variant. The output file name is always "isabelle_logo.pdf". 

76 

73741  77 
* Option "document_preprocessor" specifies the name of an executable 
78 
that is run within the document output directory, after preparing the 

79 
document sources and before the actual build process. This allows to 

80 
apply adhoc patches, without requiring a separate "build" script. 

81 

73721
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

82 
* Option "document_build" determines the document build engine, as 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

83 
defined in Isabelle/Scala (as system service). The subsequent engines 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

84 
are provided by the Isabelle distribution: 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

85 

73741  86 
 "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX 
73721
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

87 
build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

88 

73741  89 
 "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for 
73721
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

90 
special LaTeX styles) 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

91 

73741  92 
 "build": delegate to the executable "./build pdf" 
73721
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

93 

52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

94 
The presence of a "build" command within the document output directory 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

95 
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

96 
adjust session ROOT options. 
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73682
diff
changeset

97 

73741  98 
* The commandline tool "isabelle latex" has been discontinued, 
99 
INCOMPATIBILITY for old document build scripts. 

100 

101 
 Former "isabelle latex o sty" has become obsolete: Isabelle .sty 

102 
files are automatically generated within the document output 

103 
directory. 

104 

105 
 Former "isabelle latex o pdf" should be replaced by 

106 
"$ISABELLE_LUALATEX root" or "$ISABELLE_PDFLATEX root" (without 

107 
quotes), according to the intended LaTeX engine. 

108 

109 
 Former "isabelle latex o bbl" should be replaced by 

110 
"$ISABELLE_BIBTEX root" (without quotes). 

111 

112 
 Former "isabelle latex o idx" should be replaced by 

113 
"$ISABELLE_MAKEINDEX root" (without quotes). 

73724  114 

73743  115 
* Option "document_bibliography" explicitly enables the use of bibtex; 
116 
the default is to check the presence of root.bib, but it could have a 

117 
different name. 

118 

73409  119 
* Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ... 
120 
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc} 

73404  121 
(which is now also the default in "isabelle mkroot"). 
122 

73595
aece5cc9efb7
simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents:
73586
diff
changeset

123 
* Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ... 
aece5cc9efb7
simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents:
73586
diff
changeset

124 
\guillemotright from \usepackage[T1]{fontenc}  \usepackage{babel} is 
aece5cc9efb7
simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents:
73586
diff
changeset

125 
no longer required. 
aece5cc9efb7
simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents:
73586
diff
changeset

126 

73404  127 

73846  128 
*** Pure *** 
129 

130 
* "global_interpretation" is applicable in instantiation and overloading 

131 
targets and in any nested target built on top of a target supporting 

132 
"global_interpretation". 

133 

134 

73270  135 
*** HOL *** 
136 

74335  137 
* Theory HOLLibrary.Lattice_Syntax has been superseded by bundle 
138 
"lattice_syntax": it can be used in a local context via 'include' or in 

139 
a global theory via 'unbundle'. The opposite declarations are bundled as 

74348  140 
"no_lattice_syntax". Minor INCOMPATIBILITY. 
74335  141 

73829  142 
* Theory "HOLLibrary.Multiset": dedicated predicate "multiset" is gone, 
143 
use explict expression instead. Minor INCOMPATIBILITY. 

144 

145 
* Theory "HOLLibrary.Multiset": consolidated abbreviations Mempty, 

146 
Melem, not_Melem to empty_mset, member_mset, not_member_mset 

147 
respectively. Minor INCOMPATIBILITY. 

148 

149 
* Theory "HOLLibrary.Multiset": consolidated operation and fact names: 

73393  150 
inf_subset_mset ~> inter_mset 
151 
sup_subset_mset ~> union_mset 

152 
multiset_inter_def ~> inter_mset_def 

153 
sup_subset_mset_def ~> union_mset_def 

154 
multiset_inter_count ~> count_inter_mset 

155 
sup_subset_mset_count ~> count_union_mset 

156 

73829  157 
* Theory "HOLLibrary.Multiset": syntax precendence for membership 
158 
operations has been adjusted to match the corresponding precendences on 

159 
sets. Rare INCOMPATIBILITY. 

160 

73886
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreaslochbihler.de>
parents:
73876
diff
changeset

161 
* Theory "HOLLibrary.Cardinality": code generator setup based on the 
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreaslochbihler.de>
parents:
73876
diff
changeset

162 
type classes finite_UNIV and card_UNIV has been moved to 
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreaslochbihler.de>
parents:
73876
diff
changeset

163 
"HOLLibrary.Code_Cardinality", to avoid incompatibilities with 
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreaslochbihler.de>
parents:
73876
diff
changeset

164 
other code setups for sets in AFP/Containers. Applications relying on 
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreaslochbihler.de>
parents:
73876
diff
changeset

165 
this code setup should import "HOLLibrary.Code_Cardinality". Minor 
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreaslochbihler.de>
parents:
73876
diff
changeset

166 
INCOMPATIBILITY. 
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreaslochbihler.de>
parents:
73876
diff
changeset

167 

73829  168 
* Session "HOLAnalysis" and "HOLProbability": indexed products of 
169 
discrete distributions, negative binomial distribution, Hoeffding's 

170 
inequality, Chernoff bounds, Cauchyâ€“Schwarz inequality for nn_integral, 

171 
and some more small lemmas. Some theorems that were stated awkwardly 

172 
before were corrected. Minor INCOMPATIBILITY. 

73253
f6bb31879698
HOLAnalysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
73247
diff
changeset

173 

73928
3b76524f5a85
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents:
73886
diff
changeset

174 
* Session "HOLAnalysis": the complex Arg function has been identified 
3b76524f5a85
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents:
73886
diff
changeset

175 
with the function "arg" of Complex_Main, renaming arg>Arg also in the 
3b76524f5a85
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents:
73886
diff
changeset

176 
names of arg_bounded. Minor INCOMPATIBILITY. 
3b76524f5a85
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents:
73886
diff
changeset

177 

73411  178 
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to 
179 
"order.antisym" and "order.eq_iff", to coexist locally with "antisym" 

73829  180 
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant 
73411  181 
potential for change can be avoided if interpretations of type class 
182 
"order" are replaced or augmented by interpretations of locale 

183 
"ordering". 

184 

73829  185 
* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor 
73466  186 
INCOMPATIBILITY; note that for most applications less elementary lemmas 
187 
exists. 

73411  188 

73829  189 
* Theory "HOLLibrary.Permutation" has been renamed to the more specific 
190 
"HOLLibrary.List_Permutation". Note that most notions from that theory 

191 
are already present in theory "HOLCombinatorics.Permutations". 

192 
INCOMPATIBILITY. 

193 

194 
* Dedicated session "HOLCombinatorics". INCOMPATIBILITY: theories 

73477  195 
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling", 
73622  196 
"Multiset_Permutations", "Perm" have been moved there from session 
73681  197 
HOLLibrary. 
73477  198 

73829  199 
* Theory "HOLCombinatorics.Transposition" provides elementary swap 
200 
operation "transpose". 

201 

202 
* Lemma "permutes_induct" has been given stronger hypotheses and named 

203 
premises. INCOMPATIBILITY. 

204 

205 
* Combinator "Fun.swap" resolved into a mere input abbreviation in 

206 
separate theory "Transposition" in HOLCombinatorics. INCOMPATIBILITY. 

73623  207 

74097  208 
* Infix syntax for bit operations AND, OR, XOR is now organized in 
74101  209 
bundle bit_operations_syntax. INCOMPATIBILITY. 
74097  210 

73682
78044b2f001c
explicit type class operations for typespecific implementations
haftmann
parents:
73681
diff
changeset

211 
* Bit operations set_bit, unset_bit and flip_bit are now class 
73829  212 
operations. INCOMPATIBILITY. 
73682
78044b2f001c
explicit type class operations for typespecific implementations
haftmann
parents:
73681
diff
changeset

213 

74101  214 
* Theory Bit_Operations is now part of HOLMain. Minor INCOMPATIBILITY. 
215 

74123
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
74110
diff
changeset

216 
* Simplified class hierarchy for bit operations: bit operations reside 
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
74110
diff
changeset

217 
in classes (semi)ring_bit_operations, class semiring_bit_shifts is 
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
74110
diff
changeset

218 
gone. 
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
74110
diff
changeset

219 

74163  220 
* Expressions of the form "NOT (numeral _)" are not simplified by 
221 
default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq 

222 
as simp rule explicitly if needed. 

223 

73816  224 
* Abbreviation "max_word" has been moved to session Word_Lib in the AFP, 
225 
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", 

73829  226 
"setBit", "clearBit". See there further the changelog in theory Guide. 
73816  227 
INCOMPATIBILITY. 
73788  228 

74123
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
74110
diff
changeset

229 
* Reorganized classes and locales for boolean algebras. 
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
74110
diff
changeset

230 
INCOMPATIBILITY. 
7c5842b06114
clarified abstract and concrete boolean algebras
haftmann
parents:
74110
diff
changeset

231 

73869  232 
* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3, 
74101  233 
min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor 
73869  234 
INCOMPATIBILITY. 
235 

73935
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

236 
* Sledgehammer: 
74110  237 
 Removed legacy "lam_lifting" (synonym for "lifting") from option 
73935
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

238 
"lam_trans". Minor INCOMPATIBILITY. 
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

239 
 Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". 
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

240 
Minor INCOMPATIBILITY. 
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

241 
 Added "opaque_combs" to option "lam_trans": lambda expressions are rewritten 
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

242 
using combinators, but the combinators are kept opaque, i.e. without 
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

243 
definitions. 
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

244 

269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

245 
* Metis: 
269b2f976100
added documentation for changes to Sledgehammer option "lam_trans"
desharna
parents:
73928
diff
changeset

246 
 Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. 
73253
f6bb31879698
HOLAnalysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
Manuel Eberl <eberlm@in.tum.de>
parents:
73247
diff
changeset

247 

74101  248 

73287  249 
*** ML *** 
250 

74283  251 
* ML structures TFrees, TVars, Frees, Vars, Names provide scalable 
252 
operations to accumulate items from types and terms, using a fast 

253 
syntactic order. The original order of occurrences may be recovered as 

254 
well, e.g. via TFrees.list_set. 

255 

256 
* Thm.instantiate, Thm.generalize and related operations require 

257 
scalable datastructures from structure TVars, Vars, Names etc. 

258 
INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate 

259 
adoption; better use TVars.add, TVars.add_tfrees etc. for scalable 

260 
accumulation of items. 

261 

74290  262 
* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline 
263 
corresponding ML values, notably as arguments for Thm.instantiate etc. 

264 

74341  265 
* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to 
266 
corresponding functions for the objectlogic of the ML compilation 

267 
context. This supersedes older mk_Trueprop / dest_Trueprop operations. 

268 

74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

269 
* ML antiquotations for type constructors and term constants: 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

270 

b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

271 
\<^Type>\<open>c\<close> 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

272 
\<^Type>\<open>c T \<dots>\<close> \<comment> \<open>same with type arguments\<close> 
74317  273 
\<^Type>_fn\<open>c T \<dots>\<close> \<comment> \<open>fn abstraction, failure via exception TYPE\<close> 
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

274 
\<^Const>\<open>c\<close> 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

275 
\<^Const>\<open>c T \<dots>\<close> \<comment> \<open>same with type arguments\<close> 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

276 
\<^Const>\<open>c for t \<dots>\<close> \<comment> \<open>same with term arguments\<close> 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

277 
\<^Const_>\<open>c \<dots>\<close> \<comment> \<open>same for patterns: case, let, fn\<close> 
74317  278 
\<^Const>_fn\<open>c T \<dots>\<close> \<comment> \<open>fn abstraction, failure via exception TERM\<close> 
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

279 

b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

280 
Examples in HOL: 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

281 

b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

282 
val natT = \<^Type>\<open>nat\<close>; 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

283 
fun mk_funT (A, B) = \<^Type>\<open>fun A B\<close>; 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

284 
val dest_funT = fn \<^Type>\<open>fun A B\<close> => (A, B); 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

285 
fun mk_conj (A, B) = \<^Const>\<open>conj for A B\<close>; 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

286 
val dest_conj = fn \<^Const_>\<open>conj for A B\<close> => (A, B); 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

287 
fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>; 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

288 
val dest_eq = fn \<^Const_>\<open>HOL.eq T for t u\<close> => (T, (t, u)); 
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

289 

74288  290 
* The "build" combinators of various data structures help to build 
291 
content from bottomup, by applying an "add" function the "empty" value. 

292 
For example: 

293 

294 
 type 'a Symtab.table etc.: build 

74289  295 
 type 'a Names.table etc.: build 
74288  296 
 type 'a list: build and build_rev 
297 
 type Buffer.T: build and build_content 

298 

299 
For example, see src/Pure/PIDE/xml.ML: 

300 

301 
val content_of = Buffer.build_content o fold add_content; 

302 

73550
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73481
diff
changeset

303 
* ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on 
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73481
diff
changeset

304 
the given ML expression, in contrast to functions "try" and "can" that 
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73481
diff
changeset

305 
modify application of a function. 
2f6855142a8c
support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents:
73481
diff
changeset

306 

73586  307 
* ML antiquotations for conditional ML text: 
308 

309 
\<^if_linux>\<open>...\<close> 

310 
\<^if_macos>\<open>...\<close> 

311 
\<^if_windows>\<open>...\<close> 

312 
\<^if_unix>\<open>...\<close> 

313 

73287  314 
* External bash processes are always managed by Isabelle/Scala, in 
315 
contrast to Isabelle2021 where this was only done for macOS on Apple 

316 
Silicon. 

317 

318 
The main Isabelle/ML interface is Isabelle_System.bash_process with 

319 
result type Process_Result.T (resembling class Process_Result in Scala); 

320 
derived operations Isabelle_System.bash and Isabelle_System.bash_output 

321 
provide similar functionality as before. Rare INCOMPATIBILITY due to 

322 
subtle semantic differences: 

323 

324 
 Processes invoked from Isabelle/ML actually run in the context of 

325 
the Java VM of Isabelle/Scala. The settings environment and current 

326 
working directory are usually the same on both sides, but there can be 

327 
subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML). 

328 

329 
 Output via stdout and stderr is lineoriented: Unix vs. Windows 

330 
lineendings are normalized towards Unix; presence or absence of a 

331 
final newline is irrelevant. The original lines are available as 

332 
Process_Result.out_lines/err_lines; the concatenated versions 

333 
Process_Result.out/err *omit* a trailing newline (using 

334 
Library.trim_line, which was occasional seen in applications before, 

335 
but is no longer necessary). 

336 

337 
 Output needs to be plain text encoded in UTF8: Isabelle/Scala 

338 
recodes it temporarily as UTF16. This works for wellformed Unicode 

339 
text, but not for arbitrary byte strings. In such cases, the bash 

340 
script should write tempory files, managed by Isabelle/ML operations 

341 
like Isabelle_System.with_tmp_file to create a file name and 

342 
File.read to retrieve its content. 

343 

73298  344 
 Just like any other Scala function invoked from ML, 
345 
Isabelle_System.bash_process requires a proper PIDE session context. 

346 
This could be a regular batch session (e.g. "isabelle build"), a 

347 
PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g. 

348 
"isabelle dump" or "isabelle server"). Note that old "isabelle 

349 
console" or raw "isabelle process" don't have that. 

350 

73287  351 
New Process_Result.timing works as in Isabelle/Scala, based on direct 
352 
measurements of the bash_process wrapper in C: elapsed time is always 

353 
available, CPU time is only available on Linux and macOS, GC time is 

354 
unavailable. 

355 

73322  356 
* Likewise, the following Isabelle/ML system operations are run in the 
357 
context of Isabelle/Scala: 

358 

359 
 Isabelle_System.make_directory 

360 
 Isabelle_System.copy_dir 

361 
 Isabelle_System.copy_file 

362 
 Isabelle_System.copy_base_file 

73324  363 
 Isabelle_System.rm_tree 
73323  364 
 Isabelle_System.download 
73322  365 

73287  366 

73480
0e880b793db1
support repository archives (without full .hg directory);
wenzelm
parents:
73477
diff
changeset

367 
*** System *** 
0e880b793db1
support repository archives (without full .hg directory);
wenzelm
parents:
73477
diff
changeset

368 

74042  369 
* Each Isabelle component may specify a Scala/Java jar module 
74043  370 
declaratively via etc/build.props (file names are relative to the 
74042  371 
component directory). E.g. see $ISABELLE_HOME/etc/build.props with 
372 
further explanations in the "system" manual. 

373 

374 
* Commandline tool "isabelle scala_build" allows to invoke the build 

375 
process of all Scala/Java modules explicitly. Normally this is done 

376 
implicitly on demand, e.g. for "isabelle scala" or "isabelle jedit". 

377 

74071
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74043
diff
changeset

378 
* Commandline tool "isabelle scala_project" is has been improved in 
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74043
diff
changeset

379 
various ways: 
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74043
diff
changeset

380 
 sources from all components with etc/build.props are included, 
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74043
diff
changeset

381 
 sources of for the jEdit text editor and the Isabelle/jEdit 
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74043
diff
changeset

382 
plugins (jedit_base and jedit_main) are included by default, 
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74043
diff
changeset

383 
 more sources may be given on the commandline, 
b25b7c264a93
various improvements of "isabelle scala_project";
wenzelm
parents:
74043
diff
changeset

384 
 options f and D make the tool more convenient. 
74042  385 

386 
* Isabelle/jEdit is now composed more conventionally from the original 

74043  387 
jEdit text editor in $JEDIT_HOME (with minor patches), plus two Isabelle 
388 
plugins that are produced in $JEDIT_SETTINGS/jars on demand. The main 

389 
isabelle.jedit module is now part of Isabelle/Scala (as one big 

390 
$ISABELLE_SCALA_JAR). 

74042  391 

73842  392 
* ML profiling has been updated and reactivated, after some degration in 
393 
Isabelle2021: 

394 

395 
 "isabelle build o threads=1 o profiling=..." works properly 

396 
within the PIDE session context; 

397 

398 
 "isabelle profiling_report" now uses the session build database 

399 
(like "isabelle log"); 

400 

401 
 output uses nonintrusive tracing messages, instead of warnings. 

402 

73777
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" commandline (e.g. "isabelle mirabelle");
wenzelm
parents:
73774
diff
changeset

403 
* System option "system_log" specifies an optional log file for internal 
73826
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

404 
messages produced by Output.system_message in Isabelle/ML; the value 
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

405 
"true" refers to console progress of the build job. This works for 
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

406 
"isabelle build" or any derivative of it. 
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

407 

72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

408 
* System options of type string may be set to "true" using the short 
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

409 
notation of type bool. E.g. "isabelle build o system_log". 
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

410 

72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

411 
* System option "document=true" is an alias for "document=pdf" and thus 
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73816
diff
changeset

412 
can be used in the short form. E.g. "isabelle build o document". 
73774  413 

73480
0e880b793db1
support repository archives (without full .hg directory);
wenzelm
parents:
73477
diff
changeset

414 
* Commandline tool "isabelle version" supports repository archives 
73481  415 
(without full .hg directory). More options. 
73480
0e880b793db1
support repository archives (without full .hg directory);
wenzelm
parents:
73477
diff
changeset

416 

73671  417 
* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued. 
418 
Note that only Windows supports old 32 bit executables, via settings 

419 
variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be 

420 
ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64 

421 
(native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon). 

422 

73480
0e880b793db1
support repository archives (without full .hg directory);
wenzelm
parents:
73477
diff
changeset

423 

73287  424 

72972  425 
New in Isabelle2021 (February 2021) 
426 
 

71557  427 

72232
e5fcbf6dc687
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents:
72208
diff
changeset

428 
*** General *** 
e5fcbf6dc687
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents:
72208
diff
changeset

429 

73194  430 
* On macOS, the IsabelleXYZ.app directory layout now follows the other 
431 
platforms, without indirection via Contents/Resources/. INCOMPATIBILITY, 

432 
use e.g. IsabelleXYZ.app/bin/isabelle instead of former 

433 
IsabelleXYZ.app/Isabelle/bin/isabelle or 

434 
IsabelleXYZ.app/Isabelle/Contents/Resources/IsabelleXYZ/bin/isabelle. 

435 

73078  436 
* HTML presentation uses rich markup produced by Isabelle/PIDE, 
437 
resulting in more colors and links. 

438 

439 
* HTML presentation includes auxiliary files (e.g. ML) for each theory. 

73007  440 

72232
e5fcbf6dc687
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents:
72208
diff
changeset

441 
* Proof method "subst" is confined to the original subgoal range: its 
e5fcbf6dc687
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents:
72208
diff
changeset

442 
included distinct_subgoals_tac no longer affects unrelated subgoals. 
e5fcbf6dc687
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents:
72208
diff
changeset

443 
Rare INCOMPATIBILITY. 
e5fcbf6dc687
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents:
72208
diff
changeset

444 

73007  445 
* Theory_Data extend operation is obsolete and needs to be the identity 
446 
function; merge should be conservative and not reset to the empty value. 

447 
Subtle INCOMPATIBILITY and change of semantics (due to 

448 
Theory.join_theory from Isabelle2020). Special extend/merge behaviour at 

449 
the begin of a new theory can be achieved via Theory.at_begin. 

72996  450 

72232
e5fcbf6dc687
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);
wenzelm
parents:
72208
diff
changeset

451 

71932
65fd0f032a75
updated to jedit5.6pre1 (repository version 25349);
wenzelm
parents:
71927
diff
changeset

452 
*** Isabelle/jEdit Prover IDE *** 
65fd0f032a75
updated to jedit5.6pre1 (repository version 25349);
wenzelm
parents:
71927
diff
changeset

453 

73116
b84887a67cc6
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents:
73112
diff
changeset

454 
* Improved GUI lookandfeel: the portable and scalable "FlatLaf Light" 
b84887a67cc6
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents:
73112
diff
changeset

455 
is used by default on all platforms (appearance similar to IntelliJ 
b84887a67cc6
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents:
73112
diff
changeset

456 
IDEA). 
73112  457 

72946  458 
* Improved markup for theory header imports: hyperlinks for theory files 
459 
work without formal checking of content. 

460 

72950  461 
* The prover process can download auxiliary files (e.g. 'ML_file') for 
462 
theories with remote URL. This requires the external "curl" program. 

463 

72930
0cc298e29aff
added action isabelle.gotoentity to follow links in a narrow formal sense;
wenzelm
parents:
72879
diff
changeset

464 
* Action "isabelle.gotoentity" (shortcut CS+d) jumps to the definition 
0cc298e29aff
added action isabelle.gotoentity to follow links in a narrow formal sense;
wenzelm
parents:
72879
diff
changeset

465 
of the formal entity at the caret position. 
0cc298e29aff
added action isabelle.gotoentity to follow links in a narrow formal sense;
wenzelm
parents:
72879
diff
changeset

466 

72932  467 
* The visual feedback on caret entity focus is normally restricted to 
468 
definitions within the visible text area. The keyboard modifier "CS" 

469 
overrides this: then all defining and referencing positions are shown. 

470 
See also option "jedit_focus_modifier". 

471 

72249  472 
* The jEdit status line includes widgets both for JVM and ML heap usage. 
473 
Ongoing ML ongoing garbage collection is shown as "ML cleanup". 

72150  474 

475 
* The Monitor dockable provides buttons to request a full garbage 

476 
collection and sharing of live data on the ML heap. It also includes 

477 
information about the Java Runtime system. 

478 

72837  479 
* PIDE support for session ROOTS: markup for directories. 
480 

72247  481 
* Update to jedit5.6.0, the latest release. This version works properly 
482 
on macOS by default, without the special MacOSX plugin. 

71932
65fd0f032a75
updated to jedit5.6pre1 (repository version 25349);
wenzelm
parents:
71927
diff
changeset

483 

73121  484 
* Action "fullscreenmode" (shortcut F11 or S+F11) has been modified 
485 
for better approximate window size on macOS and Linux/X11. 

486 

73162
c4b688abe2c4
clarified documentation concerning macOS Big Sur;
wenzelm
parents:
73156
diff
changeset

487 
* Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode, 
c4b688abe2c4
clarified documentation concerning macOS Big Sur;
wenzelm
parents:
73156
diff
changeset

488 
but nonnative lookandfeel (FlatLaf). 
c4b688abe2c4
clarified documentation concerning macOS Big Sur;
wenzelm
parents:
73156
diff
changeset

489 

73247  490 
* Hyperlinks to various fileformats (.pdf, .png, etc.) open an external 
491 
viewer, instead of reusing the jEdit text editor. 

492 

73174  493 
* IDE support for NaprocheSAD: Proof Checking of Natural Mathematical 
494 
Documents. See also $NAPROCHE_HOME/examples for files with .ftl or 

73247  495 
.ftl.tex extension. The corresponding NaprocheSAD server process can be 
496 
disabled by setting the system option naproche_server=false and 

497 
restarting the Isabelle application. 

73224
49686e3b1909
clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents:
73194
diff
changeset

498 

71932
65fd0f032a75
updated to jedit5.6pre1 (repository version 25349);
wenzelm
parents:
71927
diff
changeset

499 

71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71901
diff
changeset

500 
*** Document preparation *** 
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71901
diff
changeset

501 

72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72581
diff
changeset

502 
* Keyword 'document_theories' within ROOT specifies theories from other 
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72581
diff
changeset

503 
sessions that should be included in the generated document source 
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72581
diff
changeset

504 
directory. This does not affect the generated session.tex: \input{...} 
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72581
diff
changeset

505 
needs to be used separately. 
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72581
diff
changeset

506 

72314  507 
* The standard LaTeX engine is now lualatex, according to settings 
508 
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old 

509 
pdflatex, but text encoding needs to conform strictly to utf8. Rare 

510 
INCOMPATIBILITY. 

511 

512 
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable: 

513 
document output is always PDF. 

514 

72763  515 
* Antiquotation @{tool} refers to Isabelle commandline tools, with 
516 
completion and formal reference to the source (external script or 

517 
internal Scala function). 

518 

71908  519 
* Antiquotation @{bash_function} refers to GNU bash functions that are 
520 
checked within the Isabelle settings environment. 

521 

522 
* Antiquotations @{scala}, @{scala_object}, @{scala_type}, 

523 
@{scala_method} refer to checked Isabelle/Scala entities. 

71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71901
diff
changeset

524 

1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71901
diff
changeset

525 

71901  526 
*** Pure *** 
527 

71924
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
71923
diff
changeset

528 
* Session PureExamples contains notable examples for Isabelle/Pure 
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
71923
diff
changeset

529 
(former entries of HOLIsar_Examples). 
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
71923
diff
changeset

530 

72739
e7c2848b78e8
refined syntax for bundle mixins for locale and class specifications
haftmann
parents:
72728
diff
changeset

531 
* Named contexts (locale and class specifications, locale and class 
73007  532 
context blocks) allow bundle mixins for the surface context. This allows 
533 
syntax notations to be organized within bundles conveniently. See theory 

534 
"HOLex.Specifications_with_bundle_mixins" for examples and the isarref 

535 
manual for syntax descriptions. 

72739
e7c2848b78e8
refined syntax for bundle mixins for locale and class specifications
haftmann
parents:
72728
diff
changeset

536 

71901  537 
* Definitions in locales produce rule which can be added as congruence 
538 
rule to protect foundational terms during simplification. 

539 

72450  540 
* Consolidated terminology and function signatures for nested targets: 
541 

73007  542 
 Local_Theory.begin_nested replaces Local_Theory.open_target 
543 

544 
 Local_Theory.end_nested replaces Local_Theory.close_target 

545 

546 
 Combination of Local_Theory.begin_nested and 

72451
e51f1733618d
replaced combinators by more conventional nesting pattern
haftmann
parents:
72450
diff
changeset

547 
Local_Theory.end_nested(_result) replaces 
73007  548 
Local_Theory.subtarget(_result) 
549 

550 
INCOMPATIBILITY. 

551 

552 
* Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY. 

72516
17dc99589a91
unified Local_Theory.init with Generic_Target.init
haftmann
parents:
72515
diff
changeset

553 

71901  554 

555 
*** HOL *** 

556 

73007  557 
* Session HOLExamples contains notable examples for Isabelle/HOL 
558 
(former entries of HOLIsar_Examples, HOLex etc.). 

559 

72478
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72470
diff
changeset

560 
* An updated version of the veriT solver is now included as Isabelle 
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72470
diff
changeset

561 
component. It can be used in the "smt" proof method via "smt (verit)" or 
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72470
diff
changeset

562 
via "declare [[smt_solver = verit]]" in the context; see also session 
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72470
diff
changeset

563 
HOLWordSMT_Examples. 
b452242dce36
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
wenzelm
parents:
72470
diff
changeset

564 

73007  565 
* Zipperposition 2.0 is now included as Isabelle component for 
72971
162b71f7e554
rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents:
72969
diff
changeset

566 
experimentation, e.g. in "sledgehammer [prover = zipperposition]". 
162b71f7e554
rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents:
72969
diff
changeset

567 

73007  568 
* Sledgehammer: 
569 
 support veriT in proof preplay 

570 
 take adventage of more cores in proof preplay 

571 

572 
* Updated the Metis prover underlying the "metis" proof method to 

573 
version 2.4 (release 20180810). The new version fixes one soundness 

574 
defect and two incompleteness defects. Very slight INCOMPATIBILITY. 

575 

72208  576 
* Nitpick/Kodkod may be invoked directly within the running 
577 
Isabelle/Scala session (instead of an external Java process): this 

578 
improves reactivity and saves resources. This experimental feature is 

73008  579 
guarded by system option "kodkod_scala" (default: true in PIDE 
580 
interaction, false in batch builds). 

72208  581 

72070  582 
* Simproc "defined_all" and rewrite rule "subst_all" perform more 
583 
aggressive substitution with variables from assumptions. 

584 
INCOMPATIBILITY, consider repairing proofs locally like this: 

585 

586 
supply subst_all [simp del] [[simproc del: defined_all]] 

587 

71901  588 
* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs" 
589 
on datatypes to "False" if either side is a proper subexpression of the 

590 
other (for any datatype with a reasonable size function). 

591 

73007  592 
* Syntax for state monad combinators fcomp and scomp is organized in 
593 
bundle state_combinator_syntax. Minor INCOMPATIBILITY. 

594 

595 
* Syntax for reflected term syntax is organized in bundle term_syntax, 

596 
discontinuing previous locale term_syntax. Minor INCOMPATIBILITY. 

597 

71901  598 
* New constant "power_int" for exponentiation with integer exponent, 
599 
written as "x powi n". 

600 

601 
* Added the "at most 1" quantifier, Uniq. 

602 

73007  603 
* For the natural numbers, "Sup {} = 0". 
72004  604 

73108
981a383610df
HOLData_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
73094
diff
changeset

605 
* New constant semiring_char gives the characteristic of any type of 
981a383610df
HOLData_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
73094
diff
changeset

606 
class semiring_1, with the convenient notation CHAR('a). For example, 
981a383610df
HOLData_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
73094
diff
changeset

607 
CHAR(nat) = CHAR(int) = CHAR(real) = 0, CHAR(17) = 17. 
981a383610df
HOLData_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
73094
diff
changeset

608 

981a383610df
HOLData_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
73094
diff
changeset

609 
* HOLComputational_Algebra.Polynomial: Definition and basic properties 
981a383610df
HOLData_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
73094
diff
changeset

610 
of algebraic integers. 
981a383610df
HOLData_Structures: added Selection and time functions for list functions
Manuel Eberl <eberlm@in.tum.de>
parents:
73094
diff
changeset

611 

71956  612 
* Library theory "Bit_Operations" with generic bit operations. 
613 

72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
72264
diff
changeset

614 
* Library theory "Signed_Division" provides operations for signed 
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
72264
diff
changeset

615 
division, instantiated for type int. 
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
72264
diff
changeset

616 

73047
ab9e27da0e85
HOLLibrary: Changed notation for sum_mset
Manuel Eberl <eberlm@in.tum.de>
parents:
73009
diff
changeset

617 
* Theory "Multiset": removed misleading notation \<Union># for sum_mset; 
73094  618 
replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also exists now. 
619 

620 
* New theory "HOLLibrary.Word" takes over material from former session 

621 
"HOLWord". INCOMPATIBILITY: need to adjust imports. 

622 

623 
* Theory "HOLLibrary.Word": Type word is restricted to bit strings 

624 
consisting of at least one bit. INCOMPATIBILITY. 

625 

626 
* Theory "HOLLibrary.Word": Bit operations NOT, AND, OR, XOR are based 

627 
on generic algebraic bit operations from theory 

628 
"HOLLibrary.Bit_Operations". INCOMPATIBILITY. 

629 

630 
* Theory "HOLLibrary.Word": Most operations on type word are set up for 

631 
transfer and lifting. INCOMPATIBILITY. 

632 

633 
* Theory "HOLLibrary.Word": Generic type conversions. INCOMPATIBILITY, 

634 
sometimes additional rewrite rules must be added to applications to get 

635 
a confluent system again. 

636 

637 
* Theory "HOLLibrary.Word": Uniform polymorphic "mask" operation for 

638 
both types int and word. INCOMPATIBILITY. 

639 

640 
* Theory "HOLLibrary.Word": Syntax for signed compare operators has 

641 
been consolidated with syntax of regular compare operators. Minor 

73007  642 
INCOMPATIBILITY. 
72388  643 

72515
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

644 
* Former session "HOLWord": Various operations dealing with bit values 
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

645 
represented as reversed lists of bools are separated into theory 
73007  646 
Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY. 
72515
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

647 

c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

648 
* Former session "HOLWord": Theory "Word_Bitwise" has been moved to AFP 
73007  649 
entry Word_Lib as theory "Bitwise". INCOMPATIBILITY. 
72515
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

650 

c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

651 
* Former session "HOLWord": Compound operation "bin_split" simplifies 
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

652 
by default into its components "drop_bit" and "take_bit". 
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

653 
INCOMPATIBILITY. 
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

654 

c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

655 
* Former session "HOLWord": Operations lsb, msb and set_bit are 
72546  656 
separated into theories Least_significant_bit, Most_significant_bit and 
657 
Generic_set_bit respectively in session Word_Lib in the AFP. 

658 
INCOMPATIBILITY. 

72515
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

659 

c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

660 
* Former session "HOLWord": Ancient int numeral representation has been 
73007  661 
factored out in separate theory "Ancient_Numeral" in session Word_Lib in 
662 
the AFP. INCOMPATIBILITY. 

72515
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

663 

c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

664 
* Former session "HOLWord": Operations "bin_last", "bin_rest", 
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

665 
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and 
73007  666 
"max_word" are now mere input abbreviations. Minor INCOMPATIBILITY. 
72515
c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

667 

c7038c397ae3
moved most material from session HOLWord to Word_Lib in the AFP
haftmann
parents:
72511
diff
changeset

668 
* Former session "HOLWord": Misc ancient material has been factored out 
73007  669 
into separate theories and moved to session Word_Lib in the AFP. See 
670 
theory "Guide" there for further information. INCOMPATIBILITY. 

71987  671 

72070  672 
* Session HOLTPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands 
673 
are in working order again, as opposed to outputting "GaveUp" on nearly 

674 
all problems. 

71959  675 

72987
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72972
diff
changeset

676 
* Session "HOLHoare": concrete syntax only for Hoare triples, not 
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72972
diff
changeset

677 
abstract language constructors. 
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72972
diff
changeset

678 

b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72972
diff
changeset

679 
* Session "HOLHoare": now provides a total correctness logic as well. 
b1be35908165
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72972
diff
changeset

680 

71901  681 

682 
*** FOL *** 

683 

684 
* Added the "at most 1" quantifier, Uniq, as in HOL. 

685 

72070  686 
* Simproc "defined_all" and rewrite rule "subst_all" have been changed 
687 
as in HOL. 

71923  688 

71901  689 

71908  690 
*** ML *** 
691 

72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72316
diff
changeset

692 
* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to 
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72316
diff
changeset

693 
registered Isabelle/Scala functions (of type String => String): 
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72316
diff
changeset

694 
invocation works via the PIDE protocol. 
71908  695 

72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72510
diff
changeset

696 
* Path.append is available as overloaded "+" operator, similar to 
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72510
diff
changeset

697 
corresponding Isabelle/Scala operation. 
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72510
diff
changeset

698 

73007  699 
* ML statistics via an external Poly/ML process: this allows monitoring 
700 
the runtime system while the ML program sleeps. 

701 

71908  702 

71715  703 
*** System *** 
704 

73007  705 
* Isabelle server allows userdefined commands via 
706 
isabelle_scala_service. 

707 

708 
* Update/rebuild external provers on currently supported OS platforms, 

709 
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1. 

710 

72879
b3e9e9e4ff74
clarified session log file: avoid erratic messages;
wenzelm
parents:
72876
diff
changeset

711 
* The commandline tool "isabelle log" prints prover messages from the 
b3e9e9e4ff74
clarified session log file: avoid erratic messages;
wenzelm
parents:
72876
diff
changeset

712 
build database of the given session, following the the order of theory 
b3e9e9e4ff74
clarified session log file: avoid erratic messages;
wenzelm
parents:
72876
diff
changeset

713 
sources, instead of erratic parallel evaluation. Consequently, the 
b3e9e9e4ff74
clarified session log file: avoid erratic messages;
wenzelm
parents:
72876
diff
changeset

714 
session log file is restricted to system messages of the overall build 
b3e9e9e4ff74
clarified session log file: avoid erratic messages;
wenzelm
parents:
72876
diff
changeset

715 
process, and thus becomes more informative. 
72876  716 

72309
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
72299
diff
changeset

717 
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings 
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
72299
diff
changeset

718 
variable. 
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
72299
diff
changeset

719 

72316
3cc6aa405858
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents:
72314
diff
changeset

720 
* The commandline tool "isabelle logo" only outputs PDF; obsolete EPS 
3cc6aa405858
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents:
72314
diff
changeset

721 
(for DVI documents) has been discontinued. Former option n has been 
3cc6aa405858
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents:
72314
diff
changeset

722 
turned into o with explicit file name. Minor INCOMPATIBILITY. 
3cc6aa405858
clarified "isabelle logo", after discontinuation of DVI output (see 564012e31db1);
wenzelm
parents:
72314
diff
changeset

723 

73172  724 
* The commandline tool "isabelle components" supports new options u 
725 
and x to manage $ISABELLE_HOME_USER/etc/components without manual 

726 
editing of Isabelle configuration files. 

727 

72162  728 
* The shell function "isabelle_directory" (within etc/settings of 
729 
components) augments the list of special directories for persistent 

730 
symbolic path names. This improves portability of heap images and 

731 
session databases. It used to be hardwired for Isabelle + AFP, but 

732 
other projects may now participate on equal terms. 

733 

72681  734 
* The commandline tool "isabelle process" now prints output to 
735 
stdout/stderr separately and incrementally, instead of just one bulk to 

736 
stdout after termination. Potential INCOMPATIBILITY for external tools. 

737 

738 
* The commandline tool "isabelle console" now supports interrupts 

739 
properly (on Linux and macOS). 

740 

72103  741 
* Batchbuilds via "isabelle build" use a PIDE session with special 
742 
protocol: this allows to invoke Isabelle/Scala operations from 

743 
Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the 

744 
java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings: 

71976  745 

746 
ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS Xmx8g" 

71975
2d658beb815b
enable pide_session by default (again), with extra JVM heap for AFP tests (see also 86e429abd38d, 026de3424c39);
wenzelm
parents:
71964
diff
changeset

747 

72728
caa182bdab7a
clarified options: batchbuild has pide_reports disabled by default (requires significant resources);
wenzelm
parents:
72684
diff
changeset

748 
This includes full PIDE markup, if option "build_pide_reports" is 
caa182bdab7a
clarified options: batchbuild has pide_reports disabled by default (requires significant resources);
wenzelm
parents:
72684
diff
changeset

749 
enabled. 
caa182bdab7a
clarified options: batchbuild has pide_reports disabled by default (requires significant resources);
wenzelm
parents:
72684
diff
changeset

750 

72679  751 
* The commandline tool "isabelle build" provides option P DIR to 
752 
produce PDF/HTML presentation in the specified directory; P: refers to 

753 
the standard directory according to ISABELLE_BROWSER_INFO / 

754 
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken 

755 
from the build database  from this or earlier builds with option 

756 
document=pdf. 

757 

72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72557
diff
changeset

758 
* The commandline tool "isabelle document" generates theory documents 
72679  759 
on the spot, using the underlying session build database (exported 
72681  760 
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former 
72679  761 
"isabelle document" tool was rather different and has been discontinued. 
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72557
diff
changeset

762 

71808  763 
* The commandline tool "isabelle sessions" explores the structure of 
764 
Isabelle sessions and prints result names in topological order (on 

765 
stdout). 

766 

71733  767 
* The Isabelle/Scala "Progress" interface changed slightly and 
768 
"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress" 

769 
instead. 

770 

771 
* General support for Isabelle/Scala system services, configured via the 

772 
shell function "isabelle_scala_service" in etc/settings (e.g. of an 

71741  773 
Isabelle component); see implementations of class 
774 
Isabelle_System.Service in Isabelle/Scala. This supersedes former 

775 
"isabelle_scala_tools" and "isabelle_file_format": minor 

776 
INCOMPATIBILITY. 

71728  777 

72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72728
diff
changeset

778 
* The syntax of theory load commands (for auxiliary files) is now 
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72728
diff
changeset

779 
specified in Isabelle/Scala, as instance of class 
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72728
diff
changeset

780 
isabelle.Command_Span.Load_Command registered via isabelle_scala_service 
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72728
diff
changeset

781 
in etc/settings. This allows more flexible schemes than just a list of 
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72728
diff
changeset

782 
file extensions. Minor INCOMPATIBILITY, e.g. see theory 
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72728
diff
changeset

783 
HOLSPARK.SPARK_Setup to emulate the old behaviour. 
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72728
diff
changeset

784 

73116
b84887a67cc6
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents:
73112
diff
changeset

785 
* JVM system property "isabelle.laf" has been discontinued; the default 
b84887a67cc6
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents:
73112
diff
changeset

786 
Swing lookandfeel is ""FlatLaf Light". 
b84887a67cc6
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
wenzelm
parents:
73112
diff
changeset

787 

72521  788 
* Isabelle/Phabricator supports Ubuntu 20.04 LTS. 
789 

71845  790 
* Isabelle/Phabricator setup has been updated to follow ongoing 
791 
development: libphutil has been discontinued. Minor INCOMPATIBILITY: 

792 
existing server installations should remove libphutil from 

793 
/usr/local/bin/isabellephabricatorupgrade and each installation root 

794 
directory (e.g. /var/www/phabricatorvcs/libphutil). 

795 

72510  796 
* Experimental support for arm64linux platform. The reference platform 
797 
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit). 

798 

73232  799 
* Support for Apple Silicon, using mostly x86_64darwin runtime 
800 
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also 

801 
some native arm64darwin executables (e.g. Java). 

73154  802 

71557  803 

71839  804 

71485  805 
New in Isabelle2020 (April 2020) 
806 
 

70265  807 

70562  808 
*** General *** 
809 

70677  810 
* Session ROOT files need to specify explicit 'directories' for import 
70681  811 
of theory files. Directories cannot be shared by different sessions. 
812 
(Recall that import of theories from other sessions works via 

813 
sessionqualified theory names, together with suitable 'sessions' 

814 
declarations in the ROOT.) 

70677  815 

70562  816 
* Internal derivations record dependencies on oracles and other theorems 
817 
accurately, including the implicit typeclass reasoning wrt. proven 

818 
class relations and type arities. In particular, the formal tagging with 

819 
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now 

820 
propagated properly to theorems depending on such type instances. 

821 

822 
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the 

823 
actual proposition that is assumed in the goal and proof context. This 

824 
requires at least Proofterm.proofs = 1 to show up in theorem 

825 
dependencies. 

826 

827 
* Command 'thm_oracles' prints all oracles used in given theorems, 

828 
covering the full graph of transitive dependencies. 

829 

70605  830 
* Command 'thm_deps' prints immediate theorem dependencies of the given 
831 
facts. The former graph visualization has been discontinued, because it 

832 
was hardly usable. 

833 

71446  834 
* Refined treatment of proof terms, including typeclass proofs for 
835 
minor objectlogics (FOL, FOLP, Sequents). 

836 

71448  837 
* The inference kernel is now confined to one main module: structure 
838 
Thm, without the former circular dependency on structure Axclass. 

839 

71545
b0b16088ccf2
allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents:
71543
diff
changeset

840 
* Mixfix annotations may use "' " (single quote followed by space) to 
b0b16088ccf2
allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents:
71543
diff
changeset

841 
separate delimiters (as documented in the isarref manual), without 
71547  842 
requiring an auxiliary empty block. A literal single quote needs to be 
71551  843 
escaped properly. Minor INCOMPATIBILITY. 
71545
b0b16088ccf2
allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
wenzelm
parents:
71543
diff
changeset

844 

70562  845 

70522  846 
*** Isar *** 
847 

848 
* The proof method combinator (subproofs m) applies the method 

849 
expression m consecutively to each subgoal, constructing individual 

850 
subproofs internally. This impacts the internal construction of proof 

851 
terms: it makes a cascade of letexpressions within the derivation tree 

852 
and may thus improve scalability. 

853 

71427  854 
* Attribute "trace_locales" activates tracing of locale instances during 
855 
roundup. It replaces the diagnostic command 'print_dependencies', which 

856 
has been discontinued. 

70608  857 

70522  858 

70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset

859 
*** Isabelle/jEdit Prover IDE *** 
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset

860 

71543  861 
* Prover IDE startup is now much faster, because theory dependencies are 
862 
no longer explored in advance. The overall session structure with its 

863 
declarations of 'directories' is sufficient to locate theory files. Thus 

864 
the "session focus" of option "isabelle jedit S" has become obsolete 

865 
(likewise for "isabelle vscode_server S"). Existing option "R" is both 

866 
sufficient and more convenient to start editing a particular session. 

867 

71497  868 
* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display 
869 
tooltip message popups, corresponding to mouse hovering with/without the 

870 
CONTROL/COMMAND key pressed. 

871 

71499  872 
* The following actions allow to navigate errors within the current 
873 
document snapshot: 

874 

875 
isabelle.firsterror (CS+a) 

71505  876 
isabelle.lasterror (CS+z) 
877 
isabelle.nexterror (CS+n) 

878 
isabelle.preverror (CS+p) 

71499  879 

71430  880 
* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax). 
881 

71520  882 
* Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM 
883 
Monitor) applies the jconsole tool on the running Isabelle/jEdit 

884 
process. This allows to monitor resource usage etc. 

885 

71543  886 
* More adequate default font sizes for Linux on HD / UHD displays: 
887 
automatic font scaling is usually absent on Linux, in contrast to 

888 
Windows and macOS. 

889 

71575  890 
* The default value for the jEdit property "view.antiAlias" (menu item 
891 
Utilities / Global Options / Text Area / Anti Aliased smooth text) is 

892 
now "subpixel HRGB", instead of former "standard". Especially on Linux 

893 
this often leads to faster text rendering, but can also cause problems 

894 
with odd color shades. An alternative is to switch back to "standard" 

895 
here, and set the following Java system property: 

896 

897 
isabelle jedit Dsun.java2d.opengl=true 

898 

899 
This can be made persistent via JEDIT_JAVA_OPTIONS in 

900 
$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop 

901 
application there is a corresponding options file in the same directory. 

902 

70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset

903 

71473
be84312a2d53
update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents:
71448
diff
changeset

904 
*** Isabelle/VSCode Prover IDE *** 
be84312a2d53
update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents:
71448
diff
changeset

905 

71484  906 
* Update of State and Preview panels to use new WebviewPanel API of 
907 
VSCode. 

71473
be84312a2d53
update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents:
71448
diff
changeset

908 

be84312a2d53
update to WebviewPanel API, following initial version by Peter Zeller;
wenzelm
parents:
71448
diff
changeset

909 

70337
48609a6af1a0
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
70300
diff
changeset

910 
*** HOL *** 
48609a6af1a0
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
70300
diff
changeset

911 

71427  912 
* Improvements of the 'lift_bnf' command: 
71264  913 
 Add support for quotient types. 
71427  914 
 Generate transfer rules for the lifted map/set/rel/pred constants 
915 
(theorems "<type>.<constant>_transfer_raw"). 

71264  916 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset

917 
* Term_XML.Encode/Decode.term uses compact representation of Const 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset

918 
"typargs" from the given declaration environment. This also makes more 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset

919 
sense for translations to lambdacalculi with explicit polymorphism. 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset

920 
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset

921 
applications. 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset

922 

70524  923 
* ASCII membership syntax concerning big operators for infimum and 
71427  924 
supremum has been discontinued. INCOMPATIBILITY. 
70524  925 

71543  926 
* Removed multiplicativity assumption from class 
927 
"normalization_semidom". Introduced various new intermediate classes 

928 
with the multiplicativity assumption; many theorem statements 

929 
(especially involving GCD/LCM) had to be adapted. This allows for a more 

930 
natural instantiation of the algebraic typeclasses for e.g. Gaussian 

931 
integers. INCOMPATIBILITY. 

932 

70524  933 
* Clear distinction between types for bits (False / True) and Z2 (0 / 
71427  934 
1): theory HOLLibrary.Bit has been renamed accordingly. 
935 
INCOMPATIBILITY. 

936 

937 
* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond 

70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset

938 
to algebra_simps and field_simps but contain more aggressive rules 
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset

939 
potentially splitting goals; algebra_split_simps roughly replaces 
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset

940 
sign_simps and field_split_simps can be used instead of divide_simps. 
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset

941 
INCOMPATIBILITY. 
70524  942 

71428  943 
* Theory HOL.Complete_Lattices: 
944 
renamed Inf_Sup > Inf_eq_Sup and Sup_Inf > Sup_eq_Inf 

945 

71434  946 
* Theory HOLLibrary.Monad_Syntax: infix operation "bind" (\<bind>) 
70524  947 
associates to the left now as is customary. 
948 

71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71166
diff
changeset

949 
* Theory HOLLibrary.Ramsey: full finite Ramsey's theorem with 
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71166
diff
changeset

950 
multiple colours and arbitrary exponents. 
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71166
diff
changeset

951 

71484  952 
* Session HOLProofs: build faster thanks to better treatment of proof 
953 
terms in Isabelle/Pure. 

71147  954 

71438  955 
* Session HOLWord: bitwise NOToperator has proper prefix syntax. Minor 
956 
INCOMPATIBILITY. 

957 

71484  958 
* Session HOLAnalysis: proof method "metric" implements a decision 
959 
procedure for simple linear statements in metric spaces. 

960 

961 
* Session HOLComplex_Analysis has been split off from HOLAnalysis. 

71149  962 

71150  963 

70525  964 
*** ML *** 
965 

966 
* Theory construction may be forked internally, the operation 

967 
Theory.join_theory recovers a single result theory. See also the example 

968 
in theory "HOLex.Join_Theory". 

969 

70565  970 
* Antiquotation @{oracle_name} inlines a formally checked oracle name. 
971 

71436  972 
* Minimal support for a softtype system within the Isabelle logical 
973 
framework (module Soft_Type_System). 

974 

71750  975 
* Former Variable.auto_fixes has been replaced by slightly more general 
976 
Proof_Context.augment: it is subject to an optional softtype system of 

977 
the underlying objectlogic. Minor INCOMPATIBILITY. 

71436  978 

71438  979 
* More scalable Export.export using XML.tree to avoid premature string 
980 
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY. 

981 

71493  982 
* Prover IDE support for the underlying Poly/ML compiler (not the basis 
983 
library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the 

984 
implementation with full markup. 

985 

70525  986 

70599  987 
*** System *** 
988 

71433  989 
* Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot> 
990 

71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset

991 
* The commandline tool "isabelle scala_project" creates a Gradle 
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset

992 
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs 
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset

993 
such as IntelliJ IDEA. 
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset

994 

71293  995 
* The commandline tool "isabelle phabricator_setup" facilitates 
996 
selfhosting of the Phabricator softwaredevelopment platform, with 

997 
support for Git, Mercurial, Subversion repositories. This helps to avoid 

998 
monoculture and to escape the gravity of centralized version control by 

999 
Github and/or Bitbucket. For further documentation, see chapter 

1000 
"Phabricator server administration" in the "system" manual. A notable 

1001 
example installation is https://isabelledev.sketis.net/. 

71134  1002 

71325  1003 
* The commandline tool "isabelle hg_setup" simplifies the setup of 
1004 
Mercurial repositories, with hosting via Phabricator or SSH file server 

1005 
access. 

1006 

70686
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset

1007 
* The commandline tool "isabelle imports" has been discontinued: strict 
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset

1008 
checking of session directories enforces sessionqualified theory names 
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset

1009 
in applications  users are responsible to specify session ROOT entries 
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset

1010 
properly. 
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset

1011 

71429  1012 
* The commandline tool "isabelle dump" and its underlying 
1013 
Isabelle/Scala module isabelle.Dump has become more scalable, by 

1014 
splitting sessions and supporting a base logic image. Minor 

1015 
INCOMPATIBILITY in options and parameters. 

1016 

71750  1017 
* The commandline tool "isabelle build_docker" has been slightly 
1018 
improved: it is now properly documented in the "system" manual. 

1019 

71438  1020 
* Isabelle/Scala support for the Linux platform (Ubuntu): packages, 
1021 
users, system services. 

1022 

1023 
* Isabelle/Scala support for proof terms (with full type/term 

1024 
information) in module isabelle.Term. 

1025 

71662  1026 
* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for 
1027 
"isabelle dump". 

1028 

70599  1029 
* Theory export via Isabelle/Scala has been reworked. The former "fact" 
1030 
name space is now split into individual "thm" items: names are 

1031 
potentially indexed, such as "foo" for singleton facts, or "bar(1)", 

1032 
"bar(2)", "bar(3)" for multifacts. Theorem dependencies are now 

1033 
exported as well: this spans an overall dependency graph of internal 

1034 
inferences; it might help to reconstruct the formal structure of theory 

71751  1035 
libraries. See also the module isabelle.Export_Theory in Isabelle/Scala. 
70599  1036 

71484  1037 
* Theory export of structured specifications, based on internal 
1038 
declarations of Spec_Rules by packages like 'definition', 'inductive', 

1039 
'primrec', 'function'. 

1040 

71428  1041 
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM 
1042 
have been discontinued  deprecated since Isabelle2018. 

1043 

71438  1044 
* More complete x86_64 platform support on macOS, notably Catalina where 
1045 
old x86 has been discontinued. 

1046 

1047 
* Update to GHC stack 2.1.3 with stackage lts13.19/ghc8.6.4. 

1048 

1049 
* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before). 

1050 

70265  1051 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset

1052 

70023  1053 
New in Isabelle2019 (June 2019) 
1054 
 

68683  1055 

69042  1056 
*** General *** 
1057 

70032  1058 
* The font collection "Isabelle DejaVu" is systematically derived from 
1059 
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif" 

69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1060 
and styles "Normal", "Bold", "Italic/Oblique", "BoldItalic/Oblique". 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1061 
The DejaVu base fonts are retricted to welldefined Unicode ranges and 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1062 
augmented by special Isabelle symbols, taken from the former 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1063 
"IsabelleText" font (which is no longer provided separately). The line 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1064 
metrics and overall rendering quality is closer to original DejaVu. 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1065 
INCOMPATIBILITY with display configuration expecting the old 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1066 
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead. 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1067 

395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1068 
* The Isabelle fonts render "\<inverse>" properly as superscript "1". 
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset

1069 

69042  1070 
* Oldstyle inner comments (* ... *) within the term language are no 
1071 
longer supported (legacy feature in Isabelle2018). 

1072 

70023  1073 
* Oldstyle {* verbatim *} tokens are explicitly marked as legacy 
1074 
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g. 

1075 
via "isabelle update_cartouches t" (available since Isabelle2015). 

1076 

70297  1077 
* Infix operators that begin or end with a "*" are now parenthesized 
1078 
without additional spaces, e.g. "(*)" instead of "( * )". Minor 

70023  1079 
INCOMPATIBILITY. 
69066  1080 

69580  1081 
* Mixfix annotations may use cartouches instead of oldstyle double 
69586
9171d1ce5a35
support for "isabelle update u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset

1082 
quotes, e.g. (infixl \<open>+\<close> 60). The commandline tool "isabelle update u 
9171d1ce5a35
support for "isabelle update u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset

1083 
mixfix_cartouches" allows to update existing theory sources 
9171d1ce5a35
support for "isabelle update u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset

1084 
automatically. 
69580  1085 

69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a letdeclaration  thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset

1086 
* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') 
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a letdeclaration  thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset

1087 
need to provide a closed expression  without trailing semicolon. Minor 
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a letdeclaration  thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset

1088 
INCOMPATIBILITY. 
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a letdeclaration  thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset

1089 

70057  1090 
* Commands 'generate_file', 'export_generated_files', and 
1091 
'compile_generated_files' support a stateless (PIDEconformant) model 

1092 
for generated sources and compiled binaries of other languages. The 

70060  1093 
compilation process is managed in Isabelle/ML, and results exported to 
70057  1094 
the session database for further use (e.g. with "isabelle export" or 
1095 
"isabelle build e"). 

1096 

69042  1097 

69189  1098 
*** Isabelle/jEdit Prover IDE *** 
1099 

70023  1100 
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle 
1101 
DejaVu" collection by default, which provides uniform rendering quality 

1102 
with the usual Isabelle symbols. Line spacing no longer needs to be 

1103 
adjusted: properties for the old IsabelleText font had "Global Options / 

70069  1104 
Text Area / Extra vertical line spacing (in pixels): 2", it now 
1105 
defaults to 1, but 0 works as well. 

70023  1106 

69780  1107 
* The jEdit File Browser is more prominent in the default GUI layout of 
1108 
Isabelle/jEdit: various virtual filesystems provide access to Isabelle 

1109 
resources, notably via "favorites:" (or "Edit Favorites"). 

1110 

70061  1111 
* Further markup and rendering for "plain text" (e.g. informal prose) 
1112 
and "raw text" (e.g. verbatim sources). This improves the visual 

1113 
appearance of formal comments inside the term language, or in general 

1114 
for repeated alternation of formal and informal text. 

1115 

69643  1116 
* Action "isabelleexportbrowser" points the File Browser to the theory 
69764  1117 
exports of the current buffer, based on the "isabelleexport:" virtual 
1118 
filesystem. The directory view needs to be reloaded manually to follow 

1119 
ongoing document processing. 

1120 

1121 
* Action "isabellesessionbrowser" points the File Browser to session 

1122 
information, based on the "isabellesession:" virtual filesystem. Its 

1123 
entries are structured according to chapter / session names, the open 

1124 
operation is redirected to the session ROOT file. 

69643  1125 

69273  1126 
* Support for userdefined fileformats via class isabelle.File_Format 
69277
258bef08b31e
support for userdefined Isabelle/Scala commandline tools;
wenzelm
parents:
69273
diff
changeset

1127 
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via 
258bef08b31e
support for userdefined Isabelle/Scala commandline tools;
wenzelm
parents:
69273
diff
changeset

1128 
the shell function "isabelle_file_format" in etc/settings (e.g. of an 
258bef08b31e
support for userdefined Isabelle/Scala commandline tools;
wenzelm
parents:
69273
diff
changeset

1129 
Isabelle component). 
69273  1130 

70023  1131 
* System option "jedit_text_overview" allows to disable the text 
1132 
overview column. 

1133 

69854
cc0b3e177b49
system option "system_heaps" supersedes various commandline options for "system build mode";
wenzelm
parents:
69829
diff
changeset

1134 
* Commandline options "s" and "u" of "isabelle jedit" override the 
cc0b3e177b49
system option "system_heaps" supersedes various commandline options for "system build mode";
wenzelm
parents:
69829
diff
changeset

1135 
default for system option "system_heaps" that determines the heap 
cc0b3e177b49
system option "system_heaps" supersedes various commandline options for "system build mode";
wenzelm
parents:
69829
diff
changeset

1136 
storage directory for "isabelle build". Option "n" is now clearly 
cc0b3e177b49
system option "system_heaps" supersedes various commandline options for "system build mode";
wenzelm
parents:
69829
diff
changeset

1137 
separated from option "s". 
cc0b3e177b49
system option "system_heaps" supersedes various commandline options for "system build mode";
wenzelm
parents:
69829
diff
changeset

1138 

70105  1139 
* The Isabelle/jEdit desktop application uses the same options as 
1140 
"isabelle jedit" for its internal "isabelle build" process: the implicit 

1141 
option "o system_heaps" (or "s") has been discontinued. This reduces 

1142 
the potential for surprise wrt. commandline tools. 

1143 

1144 
* The official download of the Isabelle/jEdit application already 

1145 
contains heap images for Isabelle/HOL within its main directory: thus 

1146 
the first encounter becomes faster and more robust (e.g. when run from a 

1147 
readonly directory). 

1148 

70072  1149 
* Isabelle DejaVu fonts are available with hinting by default, which is 
1150 
relevant for lowresolution displays. This may be disabled via system 

1151 
option "isabelle_fonts_hinted = false" in 

70075  1152 
$ISABELLE_HOME_USER/etc/preferences  it occasionally yields better 
70072  1153 
results. 
1154 

70031  1155 
* OpenJDK 11 has quite different font rendering, with better glyph 
1156 
shapes and improved subpixel antialiasing. In some situations results 

70072  1157 
might be *worse* than Oracle Java 8, though  a proper HiDPI / UHD 
1158 
display is recommended. 

70023  1159 

70258  1160 
* OpenJDK 11 supports GTK version 2.2 and 3 (according to system 
1161 
property jdk.gtk.version). The factory default is version 3, but 

1162 
ISABELLE_JAVA_SYSTEM_OPTIONS includes "Djdk.gtk.version=2.2" to make 

1163 
this more conservative (as in Java 8). Depending on the GTK theme 

1164 
configuration, "Djdk.gtk.version=3" might work better or worse. 

1165 

69189  1166 

69962
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1167 
*** Document preparation *** 
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1168 

82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1169 
* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that 
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1170 
are stripped from document output: the effect is to modify the semantic 
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1171 
presentation context or to emit markup to the PIDE document. Some 
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1172 
predefined markers are taken from the Dublin Core Metadata Initiative, 
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1173 
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that 
70281  1174 
can be retrieved from the document database. 
69962
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1175 

70140  1176 
* Oldstyle command tags %name are reinterpreted as markers with 
1177 
proofscope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as 

1178 
before. Potential INCOMPATIBILITY: multiple markers are composed in 

1179 
canonical order, resulting in a reversed list of tags in the 

1180 
presentation context. 

1181 

1182 
* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a toplevel goal 

1183 
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change 

1184 
of semantics wrt. oldstyle %name. 

69962
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1185 

70143  1186 
* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>" 
1187 
template. 

1188 

70121  1189 
* Document antiquotation option "cartouche" indicates if the output 
1190 
should be delimited as cartouche; this takes precedence over the 

1191 
analogous option "quotes". 

1192 

70122
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update u control_cartouches"  e.g. relevant for documents with thy_output_source (e.g. doc "isarref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset

1193 
* Many document antiquotations are internally categorized as "embedded" 
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update u control_cartouches"  e.g. relevant for documents with thy_output_source (e.g. doc "isarref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset

1194 
and expect one cartouche argument, which is typically used with the 
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update u control_cartouches"  e.g. relevant for documents with thy_output_source (e.g. doc "isarref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset

1195 
\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche 
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update u control_cartouches"  e.g. relevant for documents with thy_output_source (e.g. doc "isarref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset

1196 
delimiters are stripped in output of the source (antiquotation option 
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update u control_cartouches"  e.g. relevant for documents with thy_output_source (e.g. doc "isarref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset

1197 
"source"), but it is possible to enforce delimiters via option 
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update u control_cartouches"  e.g. relevant for documents with thy_output_source (e.g. doc "isarref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset

1198 
"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}. 
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update u control_cartouches"  e.g. relevant for documents with thy_output_source (e.g. doc "isarref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset

1199 

69962
82e945d472d5
documentation of document markers and reinterpreted command tags;
wenzelm
parents:
69960
diff
changeset

1200 

68879  1201 
*** Isar *** 
1202 

69045  1203 
* Implicit cases goal1, goal2, goal3, etc. have been discontinued 
1204 
(legacy feature since Isabelle2016). 

1205 

70023  1206 
* More robust treatment of structural errors: begin/end blocks take 
1207 
precedence over goal/proof. This is particularly relevant for the 

1208 
headless PIDE session and server. 

1209 

1210 
* Command keywords of kind thy_decl / thy_goal may be more specifically 

1211 
fit into the traditional document model of "definitionstatementproof" 

1212 
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. 

1213 

69045  1214 

68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1215 
*** HOL *** 
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1216 

70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical filesystem within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset

1217 
* Command 'export_code' produces output as logical files within the 
70011  1218 
theory context, as well as formal session exports that can be 
1219 
materialized via commandline tools "isabelle export" or "isabelle build 

1220 
e" (with 'export_files' in the session ROOT). Isabelle/jEdit also 

1221 
provides a virtual filesystem "isabelleexport:" that can be explored 

1222 
in the regular filebrowser. A 'file_prefix' argument allows to specify 

1223 
an explicit name prefix for the target file (SML, OCaml, Scala) or 

1224 
directory (Haskell); the default is "export" with a consecutive number 

1225 
within each theory. 

70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical filesystem within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset

1226 

435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical filesystem within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset

1227 
* Command 'export_code': the 'file' argument is now legacy and will be 
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical filesystem within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset

1228 
removed soon: writing to the physical filesystem is not welldefined in 
70011  1229 
a reactive/parallel application like Isabelle. The empty 'file' argument 
1230 
has been discontinued already: it is superseded by the filebrowser in 

1231 
Isabelle/jEdit on "isabelleexport:". Minor INCOMPATIBILITY. 

69624  1232 

70022
49e178cbf923
'code_reflect' only supports newstyle 'file_prefix';
wenzelm
parents:
70011
diff
changeset

1233 
* Command 'code_reflect' no longer supports the 'file' argument: it has 
49e178cbf923
'code_reflect' only supports newstyle 'file_prefix';
wenzelm
parents:
70011
diff
changeset

1234 
been superseded by 'file_prefix' for stateless file management as in 
49e178cbf923
'code_reflect' only supports newstyle 'file_prefix';
wenzelm
parents:
70011
diff
changeset

1235 
'export_code'. Minor INCOMPATIBILITY. 
49e178cbf923
'code_reflect' only supports newstyle 'file_prefix';
wenzelm
parents:
70011
diff
changeset

1236 

69743  1237 
* Code generation for OCaml: proper strings are used for literals. 
1238 
Minor INCOMPATIBILITY. 

1239 

69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset

1240 
* Code generation for OCaml: Zarith supersedes Nums as library for 
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset

1241 
proper integer arithmetic. The library is located via standard 
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset

1242 
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable). 
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset

1243 
The environment provided by "isabelle ocaml_setup" already contains this 
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset

1244 
tool and the required packages. Minor INCOMPATIBILITY. 
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69903
diff
changeset

1245 

69690  1246 
* Code generation for Haskell: code includes for Haskell must contain 
1247 
proper module frame, nothing is added magically any longer. 

1248 
INCOMPATIBILITY. 

1249 

70023  1250 
* Code generation: slightly more conventional syntax for 'code_stmts' 
1251 
antiquotation. Minor INCOMPATIBILITY. 

1252 

1253 
* Theory List: the precedence of the list_update operator has changed: 

1254 
"f a [n := x]" now needs to be written "(f a)[n := x]". 

1255 

1256 
* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators) 

1257 
now have the same precedence as any other prefix function symbol. Minor 

1258 
INCOMPATIBILITY. 

69861
62e47f06d22c
avoid contextsensitive simp rules whose contextfree form (image_comp) is not simp by default
haftmann
parents:
69854
diff
changeset

1259 

68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1260 
* Simplified syntax setup for big operators under image. In rare 
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1261 
situations, type conversions are not inserted implicitly any longer 
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1262 
and need to be given explicitly. Auxiliary abbreviations INFIMUM, 
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1263 
SUPREMUM, UNION, INTER should now rarely occur in output and are just 
70237  1264 
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM 
1265 
are gone INCOMPATIBILITY. 

68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1266 

70023  1267 
* The simplifier uses image_cong_simp as a congruence rule. The historic 
1268 
and not really wellformed congruence rules INF_cong*, SUP_cong*, are 

1269 
not used by default any longer. INCOMPATIBILITY; consider using declare 

1270 
image_cong_simp [cong del] in extreme situations. 

1271 

1272 
* INF_image and SUP_image are no default simp rules any longer. 

1273 
INCOMPATIBILITY, prefer image_comp as simp rule if needed. 

68938  1274 

69164  1275 
* Strong congruence rules (with =simp=> in the premises) for constant f 
69546
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69506
diff
changeset

1276 
are now uniformly called f_cong_simp, in accordance with congruence 
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69506
diff
changeset

1277 
rules produced for mappers by the datatype package. INCOMPATIBILITY. 
69164  1278 

70023  1279 
* Retired lemma card_Union_image; use the simpler card_UN_disjoint 
1280 
instead. INCOMPATIBILITY. 

1281 

1282 
* Facts sum_mset.commute and prod_mset.commute have been renamed to 

1283 
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap. 

1284 
INCOMPATIBILITY. 

1285 

1286 
* ML structure Inductive: slightly more conventional naming schema. 

1287 
Minor INCOMPATIBILITY. 

1288 

1289 
* ML: Various _global variants of specification tools have been removed. 

1290 
Minor INCOMPATIBILITY, prefer combinators 

1291 
Named_Target.theory_map[_result] to lift specifications to the global 

1292 
theory level. 

1293 

1294 
* Theory HOLLibrary.Simps_Case_Conv: 'case_of_simps' now supports 

1295 
overlapping and nonexhaustive patterns and handles arbitrarily nested 

1296 
patterns. It uses on the same algorithm as HOLLibrary.Code_Lazy, which 

1297 
assumes sequential lefttoright pattern matching. The generated 

69568
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset

1298 
equation no longer tuples the arguments on the righthand side. 
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset

1299 
INCOMPATIBILITY. 
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset

1300 

70297  1301 
* Theory HOLLibrary.Multiset: the \<Union># operator now has the same 
70023  1302 
precedence as any other prefix function symbol. 
1303 

70080  1304 
* Theory HOLLibrary.Cardinal_Notations has been discontinued in favor 
70168  1305 
of the bundle cardinal_syntax (available in theory Main). Minor 
1306 
INCOMPATIBILITY. 

70080  1307 

70023  1308 
* Session HOLLibrary and HOLNumber_Theory: Exponentiation by squaring, 
1309 
used for computing powers in class "monoid_mult" and modular 

1310 
exponentiation. 

1311 

1312 
* Session HOLComputational_Algebra: Formal Laurent series and overhaul 

1313 
of Formal power series. 

1314 

1315 
* Session HOLNumber_Theory: More material on residue rings in 

1316 
Carmichael's function, primitive roots, more properties for "ord". 

1317 

70125
b601c2c87076
type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents:
70106
diff
changeset

1318 
* Session HOLAnalysis: Better organization and much more material 
b601c2c87076
type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents:
70106
diff
changeset

1319 
at the level of abstract topological spaces. 
b601c2c87076
type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents:
70106
diff
changeset

1320 

70164
1f163f772da3
Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
paulson <lp15@cam.ac.uk>
parents:
70143
diff
changeset

1321 
* Session HOLAlgebra: Free abelian groups, etc., ported from HOL Light; 
70215
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
70175
diff
changeset

1322 
algebraic closure of a field by de Vilhena and Baillon. 
70032  1323 

70168  1324 
* Session HOLHomology has been added. It is a port of HOL Light's 
1325 
homology library, with new proofs of "invariance of domain" and related 

1326 
results. 

1327 

69099
d44cb8a3e5e0
HOLSPARK .prv files are no longer written to the filesystem;
wenzelm
parents:
69094
diff
changeset

1328 
* Session HOLSPARK: .prv files are no longer written to the 
d44cb8a3e5e0
HOLSPARK .prv files are no longer written to the filesystem;
wenzelm
parents:
69094
diff
changeset

1329 
filesystem, but exported to the session database. Results may be 
70026  1330 
retrieved via "isabelle build e HOLSPARKExamples" on the 
1331 
commandline. 

69099
d44cb8a3e5e0
HOLSPARK .prv files are no longer written to the filesystem;
wenzelm
parents:
69094
diff
changeset

1332 

70023  1333 
* Sledgehammer: 
1334 
 The URL for SystemOnTPTP, which is used by remote provers, has been 

1335 
updated. 

1336 
 The machinelearningbased filter MaSh has been optimized to take 

1337 
less time (in most cases). 

1338 

1339 
* SMT: reconstruction is now possible using the SMT solver veriT. 

1340 

70174  1341 
* Session HOLWord: 
1342 
* New theory More_Word as comprehensive entrance point. 

70175  1343 
* Merged type class bitss into type class bits. 
70174  1344 
INCOMPATIBILITY. 
1345 

68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset

1346 

68803  1347 
*** ML *** 
1348 

70023  1349 
* Command 'generate_file' allows to produce sources for other languages, 
1350 
with antiquotations in the Isabelle context (only the controlcartouche 

1351 
form). The default "cartouche" antiquotation evaluates an ML expression 

1352 
of type string and inlines the result as a string literal of the target 

1353 
language. For example, this works for Haskell as follows: 

1354 

1355 
generate_file "Pure.hs" = \<open> 

1356 
module Isabelle.Pure where 

1357 
allConst, impConst, eqConst :: String 

1358 
allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close> 

1359 
impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close> 

1360 
eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close> 

1361 
\<close> 

1362 

70082
4f936de6d9b8
tuned  prefer Isar command 'compile_generated_files';
wenzelm
parents:
70080
diff
changeset

1363 
See also commands 'export_generated_files' and 'compile_generated_files' 
4f936de6d9b8
tuned  prefer Isar command 'compile_generated_files';
wenzelm
parents:
70080
diff
changeset

1364 
to use the results. 
68803  1365 

70260  1366 
* ML evaluation (notably via command 'ML' or 'ML_file') is subject to 
68824  1367 
option ML_environment to select a named environment, such as "Isabelle" 
70260  1368 
for Isabelle/ML, or "SML" for official Standard ML. 
68803  1369 

69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset

1370 
* ML antiquotation @{master_dir} refers to the master directory of the 
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset

1371 
underlying theory, i.e. the directory of the theory file. 
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset

1372 

69470  1373 
* ML antiquotation @{verbatim} inlines its argument as string literal, 
1374 
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly 

1375 
useful. 

1376 

70023  1377 
* Local_Theory.reset is no longer available in user space. Regular 
1378 
definitional packages should use balanced blocks of 

1379 
Local_Theory.open_target versus Local_Theory.close_target instead, or 

1380 
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. 

1381 

1382 
* Original PolyML.pointerEq is retained as a convenience for tools that 

1383 
don't use Isabelle/ML (where this is called "pointer_eq"). 

69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset

1384 

69282  1385 

68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset

1386 
*** System *** 
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset

1387 

70031  1388 
* Update to OpenJDK 11: the current longterm support version of Java. 
70023  1389 

1390 
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without 

1391 
the full overhead of 64bit values everywhere. This special x86_64_32 

1392 
mode provides up to 16GB ML heap, while program code and stacks are 

1393 
allocated elsewhere. Thus approx. 5 times more memory is available for 

1394 
applications compared to old x86 mode (which is no longer used by 

1395 
Isabelle). The switch to the x86_64 CPU architecture also avoids 

1396 
compatibility problems with Linux and macOS, where 32bit applications 

1397 
are gradually phased out. 

1398 

1399 
* System option "checkpoint" has been discontinued: obsolete thanks to 

1400 
improved memory management in Poly/ML. 

1401 

1402 
* System option "system_heaps" determines where to store the session 

69854
cc0b3e177b49
system option "system_heaps" supersedes various 