author  wenzelm 
Mon, 04 Oct 2021 20:07:51 +0200  
changeset 74449  a2dcda6107d9 
parent 74437  e1b5bf983de3 
child 74451  78d1f73bbeaa 
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 

74437  7 
New in Isabelle20211 (December 2021) 
8 
 

73272  9 

73387  10 
*** General *** 
11 

74335  12 
* Commands 'syntax' and 'no_syntax' now work in a local theory context, 
74422  13 
but in contrast to 'notation' and 'no_notation' there is no proper way 
14 
to refer to local entities. Note that local syntax works well with 

15 
'bundle', e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory 

16 
Main of Isabelle/HOL. 

74335  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 

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

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

30 
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

31 
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

32 

74435  33 
* The Isabelle/Haskell library ($ISABELLE_HOME/src/Tools/Haskell) has 
34 
been significantly improved. In particular, module Isabelle.Bytes 

35 
provides type Bytes for lightweight byte strings (with optional UTF8 

36 
interpretation), similar to type string in Isabelle/ML. Isabelle symbols 

37 
now work uniformly in Isabelle/Haskell vs. Isabelle/ML vs. 

38 
Isabelle/Scala/PIDE. 

39 

73387  40 

74365
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

41 
*** Isar *** 
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

42 

b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

43 
* The improper proof command 'guess' is no longer part of by Pure, but 
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

44 
provided by the separate theory "Pureex.Guess". INCOMPATIBILITY, 
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

45 
existing applications need to import session "Pureex" and theory 
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

46 
"Pureex.Guess". Afterwards it is usually better eliminate the 'guess' 
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

47 
command, using explicit 'obtain' instead. 
b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

48 

b49bd5d9041f
improper proof command 'guess' moved to separate theory "Pureex.Guess";
wenzelm
parents:
74349
diff
changeset

49 

73616  50 
*** Isabelle/jEdit Prover IDE *** 
51 

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

53 

73876  54 
* Support for builtin font substitution of jEdit text area. 
55 

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

58 

74429
fedc0b659881
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
wenzelm
parents:
74422
diff
changeset

59 
* Addon components may provide their own jEdit plugins, via the new 
fedc0b659881
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
wenzelm
parents:
74422
diff
changeset

60 
Scala/Java module concept: instances of class 
fedc0b659881
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
wenzelm
parents:
74422
diff
changeset

61 
isabelle.Scala_Project.Plugin that are declared as "services" within 
fedc0b659881
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
wenzelm
parents:
74422
diff
changeset

62 
etc/build.props are activated on Isabelle/jEdit startup. E.g. see 
fedc0b659881
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
wenzelm
parents:
74422
diff
changeset

63 
existing isabelle.jedit.JEdit_Plugin0 (for isabelle_jedit_base.jar) and 
fedc0b659881
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
wenzelm
parents:
74422
diff
changeset

64 
isabelle.jedit.JEdit_Plugin1 (for isabelle_jedit_main.jar). 
fedc0b659881
provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
wenzelm
parents:
74422
diff
changeset

65 

73616  66 

73404  67 
*** Document preparation *** 
68 

74433
ec1774613824
support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing);
wenzelm
parents:
74429
diff
changeset

69 
* More predefined symbols: \<Parallel> \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX 
ec1774613824
support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing);
wenzelm
parents:
74429
diff
changeset

70 
package "pifont"). 
73828  71 

73830  72 
* Highquality blackboardbold symbols from font "txmia" (LaTeX package 
73828  73 
"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>. 
74 

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

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

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

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

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

81 

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

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

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

86 

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

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

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

91 

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

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

93 
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

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

95 

73741  96 
 "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

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

98 

73741  99 
 "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

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

101 

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

103 

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

104 
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

105 
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

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

107 

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

110 

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

112 
files are automatically generated within the document output 

113 
directory. 

114 

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

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

117 
quotes), according to the intended LaTeX engine. 

118 

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

120 
"$ISABELLE_BIBTEX root" (without quotes). 

121 

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

123 
"$ISABELLE_MAKEINDEX root" (without quotes). 

73724  124 

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

127 
different name. 

128 

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

73404  131 
(which is now also the default in "isabelle mkroot"). 
132 

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

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

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

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

136 

73404  137 

73846  138 
*** Pure *** 
139 

140 
* "global_interpretation" is applicable in instantiation and overloading 

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

142 
"global_interpretation". 

143 

144 

73270  145 
*** HOL *** 
146 

74422  147 
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to 
148 
"order.antisym" and "order.eq_iff", to coexist locally with "antisym" 

149 
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant 

150 
potential for change can be avoided if interpretations of type class 

151 
"order" are replaced or augmented by interpretations of locale 

152 
"ordering". 

153 

154 
* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor 

155 
INCOMPATIBILITY; note that for most applications less elementary lemmas 

156 
exists. 

157 

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

159 
premises. INCOMPATIBILITY. 

160 

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

162 
separate theory "Transposition" in HOLCombinatorics. INCOMPATIBILITY. 

163 

164 
* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in 

165 
bundle bit_operations_syntax. INCOMPATIBILITY. 

166 

167 
* Bit operations set_bit, unset_bit and flip_bit are now class 

168 
operations. INCOMPATIBILITY. 

169 

170 
* Theory Bit_Operations is now part of HOLMain. Minor INCOMPATIBILITY. 

171 

172 
* Simplified class hierarchy for bit operations: bit operations reside 

173 
in classes (semi)ring_bit_operations, class semiring_bit_shifts is 

174 
gone. 

175 

176 
* Expressions of the form "NOT (numeral _)" are not simplified by 

177 
default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq 

178 
as simp rule explicitly if needed. 

179 

180 
* Abbreviation "max_word" has been moved to session Word_Lib in the AFP, 

181 
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", 

182 
"setBit", "clearBit". See there further the changelog in theory Guide. 

183 
INCOMPATIBILITY. 

184 

185 
* Reorganized classes and locales for boolean algebras. 

186 
INCOMPATIBILITY. 

187 

188 
* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3, 

189 
min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor 

190 
INCOMPATIBILITY. 

191 

192 
* Sledgehammer: 

74437  193 
 Update of bundled provers: 
194 
E 2.6 

195 
Vampire 4.5.1 (with Open Source license) 

196 
veriT 2021.06rmx 

197 
Zipperposition 2.1 

198 
 Adjusted default provers: 

199 
cvc4 vampire verit e spass z3 zipperposition 

200 
 Removed legacy "lam_lifting" (synonym for "lifting") from option 

201 
"lam_trans". Minor INCOMPATIBILITY. 

202 
 Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor 

203 
INCOMPATIBILITY. 

204 
 Added "opaque_combs" to option "lam_trans": lambda expressions are 

205 
rewritten using combinators, but the combinators are kept opaque, 

206 
i.e. without definitions. 

74422  207 

208 
* Metis: Renamed option "hide_lams" to "opaque_lifting". Minor 

209 
INCOMPATIBILITY. 

210 

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

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

74348  214 
"no_lattice_syntax". Minor INCOMPATIBILITY. 
74335  215 

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

218 

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

220 
Melem, not_Melem to empty_mset, member_mset, not_member_mset 

221 
respectively. Minor INCOMPATIBILITY. 

222 

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

73393  224 
inf_subset_mset ~> inter_mset 
225 
sup_subset_mset ~> union_mset 

226 
multiset_inter_def ~> inter_mset_def 

227 
sup_subset_mset_def ~> union_mset_def 

228 
multiset_inter_count ~> count_inter_mset 

229 
sup_subset_mset_count ~> count_union_mset 

230 

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

233 
sets. Rare INCOMPATIBILITY. 

234 

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

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

236 
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

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

238 
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

239 
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

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

241 

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

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

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

246 
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

247 

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

248 
* Session "HOLAnalysis": the complex Arg function has been identified 
74422  249 
with the function "arg" of Complex_Main, renaming arg ~> Arg also in the 
73928
3b76524f5a85
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
paulson <lp15@cam.ac.uk>
parents:
73886
diff
changeset

250 
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

251 

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

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

255 
INCOMPATIBILITY. 

256 

257 
* Dedicated session "HOLCombinatorics". INCOMPATIBILITY: theories 

73477  258 
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling", 
73622  259 
"Multiset_Permutations", "Perm" have been moved there from session 
73681  260 
HOLLibrary. 
73477  261 

73829  262 
* Theory "HOLCombinatorics.Transposition" provides elementary swap 
263 
operation "transpose". 

264 

74101  265 

73287  266 
*** ML *** 
267 

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

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

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

272 

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

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

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

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

277 
accumulation of items. 

278 

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

281 

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

284 
context. This supersedes older mk_Trueprop / dest_Trueprop operations. 

285 

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

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

287 

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

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

289 
\<^Type>\<open>c T \<dots>\<close> \<comment> \<open>same with type arguments\<close> 
74374
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

290 
\<^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

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

292 
\<^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

293 
\<^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

294 
\<^Const_>\<open>c \<dots>\<close> \<comment> \<open>same for patterns: case, let, fn\<close> 
74374
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

295 
\<^Const_fn>\<open>c T \<dots>\<close> \<comment> \<open>fn abstraction, failure via exception TERM\<close> 
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

296 

e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

297 
The type/term arguments refer to nested ML source, which may contain 
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

298 
antiquotations recursively. The following argument syntax is supported: 
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

299 

e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

300 
 an underscore (dummy pattern) 
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

301 
 an atomic item of "embedded" syntax, e.g. identifier or cartouche 
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

302 
 an antiquotation in controlsymbol/cartouche form, e.g. \<^Type>\<open>c\<close> 
e585e5a906ba
more convenient ML arguments: avoid excessive nesting of cartouches;
wenzelm
parents:
74366
diff
changeset

303 
as short form of \<open>\<^Type>\<open>c\<close>\<close>. 
74291
b83fa8f3a271
ML antiquotations for type constructors and term constants;
wenzelm
parents:
74290
diff
changeset

304 

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

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

306 

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

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

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

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

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

314 

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

317 
For example: 

318 

319 
 type 'a Symtab.table etc.: build 

74289  320 
 type 'a Names.table etc.: build 
74288  321 
 type 'a list: build and build_rev 
322 
 type Buffer.T: build and build_content 

323 

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

325 

326 
val content_of = Buffer.build_content o fold add_content; 

327 

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

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

329 
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

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

331 

73586  332 
* ML antiquotations for conditional ML text: 
333 

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

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

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

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

338 

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

341 
Silicon. 

342 

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

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

345 
derived operations Isabelle_System.bash and Isabelle_System.bash_output 

74437  346 
provide similar functionality as before. The underlying TCP/IP server 
347 
within Isabelle/Scala is available to other programming languages as 

348 
well, notably Isabelle/Haskell. 

349 

350 
Rare INCOMPATIBILITY due to subtle semantic differences: 

73287  351 

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

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

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

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

356 

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

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

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

360 
Process_Result.out_lines/err_lines; the concatenated versions 

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

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

363 
but is no longer necessary). 

364 

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

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

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

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

369 
like Isabelle_System.with_tmp_file to create a file name and 

370 
File.read to retrieve its content. 

371 

74437  372 
 The Isabelle/Scala "bash_process" server requires a PIDE session 
373 
context. This could be a regular batch session (e.g. "isabelle 

374 
build"), a PIDE editor session (e.g. "isabelle jedit"), or headless 

375 
PIDE (e.g. "isabelle dump" or "isabelle server"). Note that old 

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

73298  377 

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

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

381 
unavailable. 

382 

74437  383 
* The following Isabelle/ML system operations are run in the context of 
384 
Isabelle/Scala, within a PIDE session context: 

73322  385 

386 
 Isabelle_System.make_directory 

387 
 Isabelle_System.copy_dir 

388 
 Isabelle_System.copy_file 

389 
 Isabelle_System.copy_base_file 

73324  390 
 Isabelle_System.rm_tree 
73323  391 
 Isabelle_System.download 
73322  392 

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

395 

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

397 
within the PIDE session context; 

398 

399 
 "isabelle profiling_report" now uses the session build database 

400 
(like "isabelle log"); 

401 

402 
 output uses nonintrusive tracing messages, instead of warnings. 

403 

73287  404 

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

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

406 

74437  407 
* Update to OpenJDK 17: the current longterm support version of Java. 
408 

74449  409 
* Perl is no longer required by Isabelle proper, and longer provided by 
410 
specific Isabelle execution environments (Docker, Cygwin on Windows). 

411 
Minor INCOMPATIBILITY, addon applications involving perl need to 

412 
provide it by different means. (Note that proper Isabelle systems 

413 
programming works via Scala/Java, without perl, python, ruby etc.). 

414 

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

419 

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

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

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

423 

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

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

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

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

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

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

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

430 
 options f and D make the tool more convenient. 
74042  431 

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

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

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

436 
$ISABELLE_SCALA_JAR). 

74042  437 

74422  438 
* Timeouts for Isabelle/ML tools are subject to system option 
439 
"timeout_scale"  this already used for the overall session build 

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

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

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

443 
in boundary cases. 

444 

445 
* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now 

446 
managed via Isabelle/Scala instead of perl; the dependency on 

447 
libwwwperl has been eliminated (notably on Linux). Rare 

448 
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties 

449 
https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/docfiles/netproperties.html 

73842  450 

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

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

452 
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

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

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

455 

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

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

457 
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

458 

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

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

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

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

462 
* Commandline tool "isabelle version" supports repository archives 
74422  463 
(without full .hg directory). It also provides more options. 
73480
0e880b793db1
support repository archives (without full .hg directory);
wenzelm
parents:
73477
diff
changeset

464 

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

467 
variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be 

468 
ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64 

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

470 

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

471 

73287  472 

72972  473 
New in Isabelle2021 (February 2021) 
474 
 

71557  475 

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

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

477 

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

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

481 
IsabelleXYZ.app/Isabelle/bin/isabelle or 

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

483 

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

486 

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

73007  488 

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

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

490 
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

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

492 

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

495 
Subtle INCOMPATIBILITY and change of semantics (due to 

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

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

72996  498 

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

499 

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

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

501 

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

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

503 
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

504 
IDEA). 
73112  505 

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

508 

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

511 

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

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

513 
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

514 

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

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

518 
See also option "jedit_focus_modifier". 

519 

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

72150  522 

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

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

525 
information about the Java Runtime system. 

526 

72837  527 
* PIDE support for session ROOTS: markup for directories. 
528 

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

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

531 

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

534 

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

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

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

537 

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

540 

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

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

545 
restarting the Isabelle application. 

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

546 

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

547 

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

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

549 

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

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

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

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

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

554 

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

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

558 
INCOMPATIBILITY. 

559 

560 
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable: 

561 
document output is always PDF. 

562 

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

565 
internal Scala function). 

566 

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

569 

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

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

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

572 

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

573 

71901  574 
*** Pure *** 
575 

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

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

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

578 

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

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

582 
"HOLex.Specifications_with_bundle_mixins" for examples and the isarref 

583 
manual for syntax descriptions. 

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

584 

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

587 

72450  588 
* Consolidated terminology and function signatures for nested targets: 
589 

73007  590 
 Local_Theory.begin_nested replaces Local_Theory.open_target 
591 

592 
 Local_Theory.end_nested replaces Local_Theory.close_target 

593 

594 
 Combination of Local_Theory.begin_nested and 

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

595 
Local_Theory.end_nested(_result) replaces 
73007  596 
Local_Theory.subtarget(_result) 
597 

598 
INCOMPATIBILITY. 

599 

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

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

601 

71901  602 

603 
*** HOL *** 

604 

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

607 

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

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

609 
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

610 
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

611 
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

612 

73007  613 
* 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

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

615 

73007  616 
* Sledgehammer: 
617 
 support veriT in proof preplay 

618 
 take adventage of more cores in proof preplay 

619 

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

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

622 
defect and two incompleteness defects. Very slight INCOMPATIBILITY. 

623 

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

626 
improves reactivity and saves resources. This experimental feature is 

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

72208  629 

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

632 
INCOMPATIBILITY, consider repairing proofs locally like this: 

633 

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

635 

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

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

639 

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

642 

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

644 
discontinuing previous locale term_syntax. Minor INCOMPATIBILITY. 

645 

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

648 

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

650 

73007  651 
* For the natural numbers, "Sup {} = 0". 
72004  652 

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

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

654 
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

655 
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

656 

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

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

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

659 

71956  660 
* Library theory "Bit_Operations" with generic bit operations. 
661 

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

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

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

664 

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

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

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

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

670 

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

672 
consisting of at least one bit. INCOMPATIBILITY. 

673 

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

675 
on generic algebraic bit operations from theory 

676 
"HOLLibrary.Bit_Operations". INCOMPATIBILITY. 

677 

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

679 
transfer and lifting. INCOMPATIBILITY. 

680 

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

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

683 
a confluent system again. 

684 

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

686 
both types int and word. INCOMPATIBILITY. 

687 

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

689 
been consolidated with syntax of regular compare operators. Minor 

73007  690 
INCOMPATIBILITY. 
72388  691 

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

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

693 
represented as reversed lists of bools are separated into theory 
73007  694 
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

695 

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

696 
* Former session "HOLWord": Theory "Word_Bitwise" has been moved to AFP 
73007  697 
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

698 

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

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

700 
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

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

702 

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

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

706 
INCOMPATIBILITY. 

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

707 

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

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

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

711 

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

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

713 
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and 
73007  714 
"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

715 

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

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

71987  719 

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

722 
all problems. 

71959  723 

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

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

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

726 

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

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

728 

71901  729 

730 
*** FOL *** 

731 

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

733 

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

71923  736 

71901  737 

71908  738 
*** ML *** 
739 

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

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

741 
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

742 
invocation works via the PIDE protocol. 
71908  743 

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

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

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

746 

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

749 

71908  750 

71715  751 
*** System *** 
752 

73007  753 
* Isabelle server allows userdefined commands via 
754 
isabelle_scala_service. 

755 

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

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

758 

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

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

760 
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

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

762 
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

763 
process, and thus becomes more informative. 
72876  764 

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

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

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

767 

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

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

769 
(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

770 
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

771 

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

774 
editing of Isabelle configuration files. 

775 

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

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

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

780 
other projects may now participate on equal terms. 

781 

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

784 
stdout after termination. Potential INCOMPATIBILITY for external tools. 

785 

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

787 
properly (on Linux and macOS). 

788 

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

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

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

71976  793 

794 
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

795 

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

796 
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

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

798 

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

801 
the standard directory according to ISABELLE_BROWSER_INFO / 

802 
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken 

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

804 
document=pdf. 

805 

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

806 
* The commandline tool "isabelle document" generates theory documents 
72679  807 
on the spot, using the underlying session build database (exported 
72681  808 
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former 
72679  809 
"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

810 

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

813 
stdout). 

814 

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

817 
instead. 

818 

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

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

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

823 
"isabelle_scala_tools" and "isabelle_file_format": minor 

824 
INCOMPATIBILITY. 

71728  825 

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

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

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

828 
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

829 
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

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

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

832 

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

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

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

835 

72521  836 
* Isabelle/Phabricator supports Ubuntu 20.04 LTS. 
837 

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

840 
existing server installations should remove libphutil from 

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

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

843 

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

846 

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

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

73154  850 

71557  851 

71839  852 

71485  853 
New in Isabelle2020 (April 2020) 
854 
 

70265  855 

70562  856 
*** General *** 
857 

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

861 
sessionqualified theory names, together with suitable 'sessions' 

862 
declarations in the ROOT.) 

70677  863 

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

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

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

868 
propagated properly to theorems depending on such type instances. 

869 

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

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

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

873 
dependencies. 

874 

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

876 
covering the full graph of transitive dependencies. 

877 

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

880 
was hardly usable. 

881 

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

884 

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

887 

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

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

889 
separate delimiters (as documented in the isarref manual), without 
71547  890 
requiring an auxiliary empty block. A literal single quote needs to be 
71551  891 
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

892 

70562  893 

70522  894 
*** Isar *** 
895 

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

897 
expression m consecutively to each subgoal, constructing individual 

898 
subproofs internally. This impacts the internal construction of proof 

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

900 
and may thus improve scalability. 

901 

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

904 
has been discontinued. 

70608  905 

70522  906 

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

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

908 

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

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

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

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

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

915 

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

918 
CONTROL/COMMAND key pressed. 

919 

71499  920 
* The following actions allow to navigate errors within the current 
921 
document snapshot: 

922 

923 
isabelle.firsterror (CS+a) 

71505  924 
isabelle.lasterror (CS+z) 
925 
isabelle.nexterror (CS+n) 

926 
isabelle.preverror (CS+p) 

71499  927 

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

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

932 
process. This allows to monitor resource usage etc. 

933 

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

936 
Windows and macOS. 

937 

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

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

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

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

943 
here, and set the following Java system property: 

944 

945 
isabelle jedit Dsun.java2d.opengl=true 

946 

947 
This can be made persistent via JEDIT_JAVA_OPTIONS in 

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

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

950 

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

951 

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

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

953 

71484  954 
* Update of State and Preview panels to use new WebviewPanel API of 
955 
VSCode. 

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

956 

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

957 

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

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

959 

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

71264  964 

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

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

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

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

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

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

970 

70524  971 
* ASCII membership syntax concerning big operators for infimum and 
71427  972 
supremum has been discontinued. INCOMPATIBILITY. 
70524  973 

71543  974 
* Removed multiplicativity assumption from class 
975 
"normalization_semidom". Introduced various new intermediate classes 

976 
with the multiplicativity assumption; many theorem statements 

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

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

979 
integers. INCOMPATIBILITY. 

980 

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

984 

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

986 
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

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

988 
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

989 
INCOMPATIBILITY. 
70524  990 

71428  991 
* Theory HOL.Complete_Lattices: 
992 
renamed Inf_Sup > Inf_eq_Sup and Sup_Inf > Sup_eq_Inf 

993 

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

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

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

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

999 

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

71147  1002 

71438  1003 
* Session HOLWord: bitwise NOToperator has proper prefix syntax. Minor 
1004 
INCOMPATIBILITY. 

1005 

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

1008 

1009 
* Session HOLComplex_Analysis has been split off from HOLAnalysis. 

71149  1010 

71150  1011 

70525  1012 
*** ML *** 
1013 

1014 
* Theory construction may be forked internally, the operation 

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

1016 
in theory "HOLex.Join_Theory". 

1017 

70565  1018 
* Antiquotation @{oracle_name} inlines a formally checked oracle name. 
1019 

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

1022 

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

1025 
the underlying objectlogic. Minor INCOMPATIBILITY. 

71436  1026 

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

1029 

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

1032 
implementation with full markup. 

1033 

70525  1034 

70599  1035 
*** System *** 
1036 

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

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

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

1040 
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

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

1042 

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

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

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

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

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

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

71134  1050 

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

1053 
access. 

1054 

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

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

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

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

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

1059 

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

1062 
splitting sessions and supporting a base logic image. Minor 

1063 
INCOMPATIBILITY in options and parameters. 

1064 

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

1067 

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

1070 

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

1072 
information) in module isabelle.Term. 

1073 

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

1076 

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

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

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

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

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

71751  1083 
libraries. See also the module isabelle.Export_Theory in Isabelle/Scala. 
70599  1084 

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

1087 
'primrec', 'function'. 

1088 

71428  1089 
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM 
1090 
have been discontinued  deprecated since Isabelle2018. 

1091 

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

1094 

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

1096 

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

1098 

70265  1099 

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

1100 

70023  1101 
New in Isabelle2019 (June 2019) 
1102 
 

68683  1103 

69042  1104 
*** General *** 
1105 

70032  1106 
* The font collection "Isabelle DejaVu" is systematically derived from 
1107 
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

1108 
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

1109 
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

1110 
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

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

1112 
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

1113 
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

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

1115 

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

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

1117 

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

1120 

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

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

1124 

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

70023  1127 
INCOMPATIBILITY. 
69066  1128 

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

1130 
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

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

1132 
automatically. 
69580  1133 

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

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

1135 
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

1136 
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

1137 

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

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

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

1144 

69042  1145 

69189  1146 
*** Isabelle/jEdit Prover IDE *** 
1147 

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

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

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

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

70023  1154 

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

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

1158 

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

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

1162 
for repeated alternation of formal and informal text. 

1163 

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

1167 
ongoing document processing. 

1168 

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

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

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

1172 
operation is redirected to the session ROOT file. 

69643  1173 

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

1175 
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

1176 
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

1177 
Isabelle component). 
69273  1178 

70023  1179 
* System option "jedit_text_overview" allows to disable the text 
1180 
overview column. 

1181 

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

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

1183 
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

1184 
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

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

1186 

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

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

1190 
the potential for surprise wrt. commandline tools. 

1191 

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

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

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

1195 
readonly directory). 

1196 

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

1199 
option "isabelle_fonts_hinted = false" in 

70075  1200 
$ISABELLE_HOME_USER/etc/preferences  it occasionally yields better 
70072  1201 
results. 
1202 

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

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

70023  1207 

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

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

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

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

1213 

69189  1214 

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

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

1216 

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

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

1218 
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

1219 
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

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

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

1223 

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

1226 
before. Potential INCOMPATIBILITY: multiple markers are composed in 

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

1228 
presentation context. 

1229 

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

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

1232 
of semantics wrt. oldstyle %name. 

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

1233 

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

1236 

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

1239 
analogous option "quotes". 

1240 

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

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

1242 
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

1243 
\<^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

1244 
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

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

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

1247 

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

1248 

68879  1249 
*** Isar *** 
1250 

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

1253 

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

1256 
headless PIDE session and server. 

1257 

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

1259 
fit into the traditional document model of "definitionstatementproof" 

1260 
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. 

1261 

69045  1262 

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

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

1264 

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

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

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

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

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

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

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

1273 
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

1274 

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

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

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

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

69624  1280 

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

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

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

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

1284 

69743  1285 
* Code generation for OCaml: proper strings are used for literals. 
1286 
Minor INCOMPATIBILITY. 

1287 

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

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

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

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

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

1292 
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

1293 

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

1296 
INCOMPATIBILITY. 

1297 

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

1300 

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

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

1303 

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

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

1306 
INCOMPATIBILITY. 

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

1307 

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

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

1309 
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

1310 
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

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

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

1314 

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

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

1318 
image_cong_simp [cong del] in extreme situations. 

1319 

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

1321 
INCOMPATIBILITY, prefer image_comp as simp rule if needed. 

68938  1322 

69164  1323 
* 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

1324 
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

1325 
rules produced for mappers by the datatype package. INCOMPATIBILITY. 
69164  1326 

70023  1327 
* Retired lemma card_Union_image; use the simpler card_UN_disjoint 
1328 
instead. INCOMPATIBILITY. 

1329 

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

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

1332 
INCOMPATIBILITY. 

1333 

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

1335 
Minor INCOMPATIBILITY. 

1336 

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

1338 
Minor INCOMPATIBILITY, prefer combinators 

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

1340 
theory level. 

1341 

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

1343 
overlapping and nonexhaustive patterns and handles arbitrarily nested 

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

1345 
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

1346 
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

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

1348 

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

70080  1352 
* Theory HOLLibrary.Cardinal_Notations has been discontinued in favor 
70168  1353 
of the bundle cardinal_syntax (available in theory Main). Minor 
1354 
INCOMPATIBILITY. 

70080  1355 

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

1358 
exponentiation. 

1359 

1360 
* Session HOLComputational_Algebra: Formal Laurent series and overhaul 

1361 
of Formal power series. 

1362 

1363 
* Session HOLNumber_Theory: More material on residue rings in 

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

1365 

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

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

1367 
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

1368 

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

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

1370 
algebraic closure of a field by de Vilhena and Baillon. 
70032  1371 

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

1374 
results. 

1375 

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

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

1377 
filesystem, but exported to the session database. Results may be 
70026  1378 
retrieved via "isabelle build e HOLSPARKExamples" on the 
1379 
commandline. 

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

1380 

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

1383 
updated. 

1384 
 The machinelearningbased filter MaSh has been optimized to take 

1385 
less time (in most cases). 

1386 

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

1388 

70174  1389 
* Session HOLWord: 
1390 
* New theory More_Word as comprehensive entrance point. 

70175  1391 
* Merged type class bitss into type class bits. 
70174  1392 
INCOMPATIBILITY. 
1393 

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

1394 

68803  1395 
*** ML *** 
1396 

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

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

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

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

1402 

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