author  wenzelm 
Tue, 17 Jan 2017 16:11:47 +0100  
changeset 64917  5db5b8cf6dc6 
parent 64900  3687036107cd 
child 64986  b81a048960a3 
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 

64603  6 

64439  7 
New in this Isabelle version 
8 
 

9 

64602  10 
*** Prover IDE  Isabelle/Scala/jEdit *** 
11 

12 
* Commandline invocation "isabelle jedit R l LOGIC" opens the ROOT 

13 
entry of the specified logic session in the editor, while its parent is 

14 
used for formal checking. 

15 

64842  16 
* The PIDE document model maintains file content independently of the 
17 
status of jEdit editor buffers. Reloading jEdit buffers no longer causes 

18 
changes of formal document content. Theory dependencies are always 

19 
resolved internally, without the need for corresponding editor buffers. 

20 
The system option "jedit_auto_load" has been discontinued: it is 

21 
effectively always enabled. 

22 

64867  23 
* The Theories dockable provides a "Purge" button, in order to restrict 
24 
the document model to theories that are required for open editor 

25 
buffers. 

26 

64602  27 

64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

28 
*** HOL *** 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

29 

64917  30 
* Some old and rarely used ASCII replacement syntax has been removed. 
31 
INCOMPATIBILITY, standard syntax with symbols should be used instead. 

32 
The subsequent commands help to reproduce the old forms, e.g. to 

33 
simplify porting old theories: 

34 

35 
syntax (ASCII) 

36 
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10) 

37 
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PI _:_./ _)" 10) 

38 
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3%_:_./ _)" [0,0,3] 3) 

39 

64632  40 
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively. 
41 
INCOMPATIBILITY. 

42 

64787  43 
* Dropped abbreviations transP, antisymP, single_valuedP; 
64634  44 
use constants transp, antisymp, single_valuedp instead. 
45 
INCOMPATIBILITY. 

64633
5ebcf6c525f1
prefer existing logical constant over abbreviation
haftmann
parents:
64632
diff
changeset

46 

64785  47 
* Algebraic type class hierarchy of euclidean (semi)rings in HOL: 
48 
euclidean_(semi)ring, euclidean_(semi)ring_cancel, 

49 
unique_euclidean_(semi)ring; instantiation requires 

50 
provision of a euclidean size. 

51 

64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

52 
* Reworking of theory Euclidean_Algorithm in session HOLNumber_Theory: 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

53 
 Euclidean induction is available as rule eucl_induct; 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

54 
 Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm, 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

55 
Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

56 
easy instantiation of euclidean (semi)rings as GCD (semi)rings. 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

57 
 Coefficients obtained by extended euclidean algorithm are 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

58 
available as "bezout_coefficients". 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

59 
INCOMPATIBILITY. 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64785
diff
changeset

60 

64787  61 
* Named collection mod_simps covers various congruence rules 
62 
concerning mod, replacing former zmod_simps. 

63 
INCOMPATIBILITY. 

64 

64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

65 
* Swapped orientation of congruence rules mod_add_left_eq, 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

66 
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

67 
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

68 
mod_diff_eq. INCOMPATIBILITY. 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

69 

50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

70 
* Generalized some facts: 
64876  71 
measure_induct_rule 
72 
measure_induct 

64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

73 
zminus_zmod ~> mod_minus_eq 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

74 
zdiff_zmod_left ~> mod_diff_left_eq 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

75 
zdiff_zmod_right ~> mod_diff_right_eq 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

76 
zmod_eq_dvd_iff ~> mod_eq_dvd_iff 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

77 
INCOMPATIBILITY. 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

78 

64532
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

79 
* (Co)datatype package: 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

80 
 The 'size_gen_o_map' lemma is no longer generated for datatypes 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

81 
with type class annotations. As a result, the tactic that derives 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

82 
it no longer fails on nested datatypes. Slight INCOMPATIBILITY. 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

83 

64898  84 
* Session HOLAnalysis: more material involving arcs, paths, covering 
85 
spaces, innessential maps, retracts. Major results include the Jordan 

86 
Curve Theorem. 

64846  87 

64543
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64532
diff
changeset

88 
* The theorem in Permutations has been renamed: 
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64532
diff
changeset

89 
bij_swap_ompose_bij ~> bij_swap_compose_bij 
64602  90 

60331  91 

64844  92 
*** System *** 
93 

94 
* Prover IDE support for the Visual Studio Code editor and language 

95 
server protocol, via the "isabelle vscode_server" tool (see also 

96 
src/Tools/VSCode/README.md). The example application within the VS code 

97 
editor is called "Isabelle" and available from its online repository 

98 
(the "Marketplace"). It serves as example for further potential IDE 

99 
frontends. 

100 

64900  101 
* ISABELLE_SCALA_BUILD_OPTIONS has been renamed to 
102 
ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY. 

103 

104 

64844  105 

64072  106 
New in Isabelle20161 (December 2016) 
107 
 

62216  108 

62440  109 
*** General *** 
110 

64390  111 
* Splitter in proof methods "simp", "auto" and friends: 
112 
 The syntax "split add" has been discontinued, use plain "split", 

113 
INCOMPATIBILITY. 

114 
 For situations with many conditional or case expressions, there is 

115 
an alternative splitting strategy that can be much faster. It is 

116 
selected by writing "split!" instead of "split". It applies safe 

117 
introduction and elimination rules after each split rule. As a 

118 
result the subgoal may be split into several subgoals. 

119 

63273  120 
* Command 'bundle' provides a local theory target to define a bundle 
121 
from the body of specification commands (such as 'declare', 

122 
'declaration', 'notation', 'lemmas', 'lemma'). For example: 

123 

124 
bundle foo 

125 
begin 

126 
declare a [simp] 

127 
declare b [intro] 

128 
end 

63272  129 

63282  130 
* Command 'unbundle' is like 'include', but works within a local theory 
131 
context. Unlike "context includes ... begin", the effect of 'unbundle' 

132 
on the target context persists, until different declarations are given. 

133 

63977  134 
* Simplified outer syntax: uniform category "name" includes long 
135 
identifiers. Former "xname" / "nameref" / "name reference" has been 

136 
discontinued. 

137 

138 
* Embedded content (e.g. the inner syntax of types, terms, props) may be 

139 
delimited uniformly via cartouches. This works better than oldfashioned 

140 
quotes when sublanguages are nested. 

141 

142 
* Mixfix annotations support general block properties, with syntax 

143 
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent", 

144 
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent 

145 
to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks 

146 
is superseded by "(\<open>unbreabable\<close>"  rare INCOMPATIBILITY. 

63650  147 

63383  148 
* Proof method "blast" is more robust wrt. corner cases of Pure 
149 
statements without objectlogic judgment. 

150 

63624
994d1a1105ef
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
wenzelm
parents:
63610
diff
changeset

151 
* Commands 'prf' and 'full_prf' are somewhat more informative (again): 
63977  152 
proof terms are reconstructed and cleaned from administrative thm nodes. 
153 

154 
* Code generator: config option "code_timing" triggers measurements of 

155 
different phases of code generation. See src/HOL/ex/Code_Timing.thy for 

156 
examples. 

157 

158 
* Code generator: implicits in Scala (stemming from type class 

159 
instances) are generated into companion object of corresponding type 

160 
class, to resolve some situations where ambiguities may occur. 

161 

64390  162 
* Solve direct: option "solve_direct_strict_warnings" gives explicit 
163 
warnings for lemma statements with trivial proofs. 

64013
048b7dbfdfa3
option to report results of solve_direct as explicit warnings
haftmann
parents:
63995
diff
changeset

164 

64602  165 

62904  166 
*** Prover IDE  Isabelle/Scala/jEdit *** 
167 

64527  168 
* More aggressive flushing of machinegenerated input, according to 
169 
system option editor_generated_input_delay (in addition to existing 

170 
editor_input_delay for regular user edits). This may affect overall PIDE 

171 
reactivity and CPU usage. 

172 

64390  173 
* Syntactic indentation according to Isabelle outer syntax. Action 
174 
"indentlines" (shortcut C+i) indents the current line according to 

175 
command keywords and some command substructure. Action 

176 
"isabelle.newline" (shortcut ENTER) indents the old and the new line 

177 
according to command keywords only; see also option 

178 
"jedit_indent_newline". 

179 

180 
* Semantic indentation for unstructured proof scripts ('apply' etc.) via 

181 
number of subgoals. This requires information of ongoing document 

182 
processing and may thus lag behind, when the user is editing too 

183 
quickly; see also option "jedit_script_indent" and 

184 
"jedit_script_indent_limit". 

185 

186 
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' 

187 
are treated as delimiters for fold structure; 'begin' and 'end' 

188 
structure of theory specifications is treated as well. 

189 

190 
* Command 'proof' provides information about proof outline with cases, 

191 
e.g. for proof methods "cases", "induct", "goal_cases". 

192 

193 
* Completion templates for commands involving "begin ... end" blocks, 

194 
e.g. 'context', 'notepad'. 

195 

196 
* Sidekick parser "isabellecontext" shows nesting of context blocks 

197 
according to 'begin' and 'end' structure. 

198 

63977  199 
* Highlighting of entity def/ref positions wrt. cursor. 
200 

201 
* Action "isabelle.selectentity" (shortcut CS+ENTER) selects all 

64514  202 
occurrences of the formal entity at the caret position. This facilitates 
63977  203 
systematic renaming. 
204 

205 
* PIDE document markup works across multiple Isar commands, e.g. the 

206 
results established at the end of a proof are properly identified in the 

207 
theorem statement. 

208 

209 
* Cartouche abbreviations work both for " and ` to accomodate typical 

210 
situations where old ASCII notation may be updated. 

211 

63875  212 
* Dockable window "Symbols" also provides access to 'abbrevs' from the 
213 
outer syntax of the current theory buffer. This provides clickable 

214 
syntax templates, including entries with empty abbrevs name (which are 

215 
inaccessible via keyboard completion). 

216 

63022  217 
* IDE support for the Isabelle/Pure bootstrap process, with the 
218 
following independent stages: 

219 

220 
src/Pure/ROOT0.ML 

221 
src/Pure/ROOT.ML 

222 
src/Pure/Pure.thy 

223 
src/Pure/ML_Bootstrap.thy 

224 

225 
The ML ROOT files act like quasitheories in the context of theory 

226 
ML_Bootstrap: this allows continuous checking of all loaded ML files. 

227 
The theory files are presented with a modified header to import Pure 

228 
from the running Isabelle instance. Results from changed versions of 

229 
each stage are *not* propagated to the next stage, and isolated from the 

230 
actual Isabelle/Pure that runs the IDE itself. The sequential 

63307  231 
dependencies of the above files are only observed for batch build. 
62904  232 

63977  233 
* Isabelle/ML and Standard ML files are presented in Sidekick with the 
234 
tree structure of section headings: this special comment format is 

235 
described in "implementation" chapter 0, e.g. (*** section ***). 

63461  236 

63581  237 
* Additional abbreviations for syntactic completion may be specified 
63871  238 
within the theory header as 'abbrevs'. The theory syntax for 'keywords' 
239 
has been simplified accordingly: optional abbrevs need to go into the 

240 
new 'abbrevs' section. 

241 

242 
* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and 

243 
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor 

244 
INCOMPATIBILITY, use 'abbrevs' within theory header instead. 

63579  245 

64390  246 
* Action "isabelle.keymapmerge" asks the user to resolve pending 
247 
Isabelle keymap changes that are in conflict with the current jEdit 

248 
keymap; nonconflicting changes are always applied implicitly. This 

249 
action is automatically invoked on Isabelle/jEdit startup and thus 

250 
increases chances that users see new keyboard shortcuts when reusing 

251 
old keymaps. 

252 

63675  253 
* ML and document antiquotations for filesystems paths are more uniform 
254 
and diverse: 

255 

256 
@{path NAME}  no filesystem check 

257 
@{file NAME}  check for plain file 

258 
@{dir NAME}  check for directory 

259 

260 
Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may 

261 
have to be changed. 

63669  262 

263 

63977  264 
*** Document preparation *** 
265 

266 
* New symbol \<circle>, e.g. for temporal operator. 

267 

64073  268 
* New document and ML antiquotation @{locale} for locales, similar to 
269 
existing antiquotation @{class}. 

270 

63977  271 
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close>  
272 
this allows special forms of document output. 

273 

274 
* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control 

275 
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its 

276 
derivatives. 

277 

278 
* \<^raw:...> symbols are no longer supported. 

279 

280 
* Old 'header' command is no longer supported (legacy since 

281 
Isabelle2015). 

282 

283 

62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

284 
*** Isar *** 
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

285 

63180  286 
* Many specification elements support structured statements with 'if' / 
287 
'for' eigencontext, e.g. 'axiomatization', 'abbreviation', 

288 
'definition', 'inductive', 'function'. 

289 

63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

290 
* Toplevel theorem statements support eigencontext notation with 'if' / 
63284  291 
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

292 
traditional long statement form (in prefix). Local premises are called 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

293 
"that" or "assms", respectively. Empty premises are *not* bound in the 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

294 
context: INCOMPATIBILITY. 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

295 

63039  296 
* Command 'define' introduces a local (nonpolymorphic) definition, with 
297 
optional abstraction over local parameters. The syntax resembles 

63043  298 
'definition' and 'obtain'. It fits better into the Isar language than 
299 
old 'def', which is now a legacy feature. 

63039  300 

63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

301 
* Command 'obtain' supports structured statements with 'if' / 'for' 
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

302 
context. 
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

303 

62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

304 
* Command '\<proof>' is an alias for 'sorry', with different 
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

305 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  306 

63977  307 
* The defining position of a literal fact \<open>prop\<close> is maintained more 
308 
carefully, and made accessible as hyperlink in the Prover IDE. 

309 

310 
* Commands 'finally' and 'ultimately' used to expose the result as 

311 
literal fact: this accidental behaviour has been discontinued. Rare 

312 
INCOMPATIBILITY, use more explicit means to refer to facts in Isar. 

313 

314 
* Command 'axiomatization' has become more restrictive to correspond 

315 
better to internal axioms as singleton facts with mandatory name. Minor 

316 
INCOMPATIBILITY. 

62939  317 

63259  318 
* Proof methods may refer to the main facts via the dynamic fact 
319 
"method_facts". This is particularly useful for Eisbach method 

320 
definitions. 

321 

63527  322 
* Proof method "use" allows to modify the main facts of a given method 
323 
expression, e.g. 

63259  324 

325 
(use facts in simp) 

326 
(use facts in \<open>simp add: ...\<close>) 

327 

63977  328 
* The old proof method "default" has been removed (legacy since 
329 
Isabelle2016). INCOMPATIBILITY, use "standard" instead. 

330 

62216  331 

63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset

332 
*** Pure *** 
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset

333 

63977  334 
* Pure provides basic versions of proof methods "simp" and "simp_all" 
335 
that only know about metaequality (==). Potential INCOMPATIBILITY in 

336 
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order 

337 
is relevant to avoid confusion of Pure.simp vs. HOL.simp. 

338 

339 
* The command 'unfolding' and proof method "unfold" include a second 

340 
stage where given equations are passed through the attribute "abs_def" 

341 
before rewriting. This ensures that definitions are fully expanded, 

342 
regardless of the actual parameters that are provided. Rare 

343 
INCOMPATIBILITY in some corner cases: use proof method (simp only:) 

344 
instead, or declare [[unfold_abs_def = false]] in the proof context. 

345 

346 
* Typeinference improves sorts of newly introduced type variables for 

347 
the objectlogic, using its base sort (i.e. HOL.type for Isabelle/HOL). 

348 
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context 

349 
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare 

350 
INCOMPATIBILITY, need to provide explicit type constraints for Pure 

351 
types where this is really intended. 

63350
705229ed856e
compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents:
63343
diff
changeset

352 

63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset

353 

62327  354 
*** HOL *** 
355 

63977  356 
* New proof method "argo" using the builtin Argo solver based on SMT 
357 
technology. The method can be used to prove goals of quantifierfree 

358 
propositional logic, goals based on a combination of quantifierfree 

359 
propositional logic with equality, and goals based on a combination of 

360 
quantifierfree propositional logic with linear real arithmetic 

361 
including min/max/abs. See HOL/ex/Argo_Examples.thy for examples. 

362 

64390  363 
* The new "nunchaku" program integrates the Nunchaku model finder. The 
364 
tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details. 

365 

63977  366 
* Metis: The problem encoding has changed very slightly. This might 
63785  367 
break existing proofs. INCOMPATIBILITY. 
368 

63116  369 
* Sledgehammer: 
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset

370 
 The MaSh relevance filter is now faster than before. 
63116  371 
 Produce syntactically correct Vampire 4.0 problem files. 
372 

62327  373 
* (Co)datatype package: 
62693  374 
 New commands for defining corecursive functions and reasoning about 
375 
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', 

376 
'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof 

62842  377 
method. See 'isabelle doc corec'. 
63977  378 
 The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a firstclass 
63855  379 
citizen in bounded natural functors. 
62693  380 
 'primrec' now allows nested calls through the predicator in addition 
62327  381 
to the map function. 
63855  382 
 'bnf' automatically discharges reflexive proof obligations. 
62693  383 
 'bnf' outputs a slightly modified proof obligation expressing rel in 
62332  384 
terms of map and set 
63855  385 
(not giving a specification for rel makes this one reflexive). 
62693  386 
 'bnf' outputs a new proof obligation expressing pred in terms of set 
63855  387 
(not giving a specification for pred makes this one reflexive). 
388 
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. 

62335  389 
 Renamed lemmas: 
390 
rel_prod_apply ~> rel_prod_inject 

391 
pred_prod_apply ~> pred_prod_inject 

392 
INCOMPATIBILITY. 

62536
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
62525
diff
changeset

393 
 The "size" plugin has been made compatible again with locales. 
63855  394 
 The theorems about "rel" and "set" may have a slightly different (but 
395 
equivalent) form. 

396 
INCOMPATIBILITY. 

62327  397 

63977  398 
* The 'coinductive' command produces a proper coinduction rule for 
399 
mutual coinductive predicates. This new rule replaces the old rule, 

400 
which exposed details of the internal fixpoint construction and was 

401 
hard to use. INCOMPATIBILITY. 

402 

403 
* New abbreviations for negated existence (but not bounded existence): 

404 

405 
\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) 

406 
\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) 

407 

408 
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" 

409 
has been removed for output. It is retained for input only, until it is 

410 
eliminated altogether. 

411 

412 
* The unique existence quantifier no longer provides 'binder' syntax, 

413 
but uses syntax translations (as for bounded unique existence). Thus 

414 
iterated quantification \<exists>!x y. P x y with its slightly confusing 

415 
sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead, 

416 
pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y 

417 
(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential 

418 
INCOMPATIBILITY in rare situations. 

419 

420 
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic 

421 
INCOMPATIBILITY. 

422 

64390  423 
* Renamed constants and corresponding theorems: 
424 

425 
setsum ~> sum 

426 
setprod ~> prod 

427 
listsum ~> sum_list 

428 
listprod ~> prod_list 

429 

430 
INCOMPATIBILITY. 

431 

432 
* Sligthly more standardized theorem names: 

433 
sgn_times ~> sgn_mult 

434 
sgn_mult' ~> Real_Vector_Spaces.sgn_mult 

435 
divide_zero_left ~> div_0 

436 
zero_mod_left ~> mod_0 

437 
divide_zero ~> div_by_0 

438 
divide_1 ~> div_by_1 

439 
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left 

440 
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left 

441 
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right 

442 
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right 

443 
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left 

444 
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right 

445 
mod_div_equality ~> div_mult_mod_eq 

446 
mod_div_equality2 ~> mult_div_mod_eq 

447 
mod_div_equality3 ~> mod_div_mult_eq 

448 
mod_div_equality4 ~> mod_mult_div_eq 

449 
minus_div_eq_mod ~> minus_div_mult_eq_mod 

450 
minus_div_eq_mod2 ~> minus_mult_div_eq_mod 

451 
minus_mod_eq_div ~> minus_mod_eq_div_mult 

452 
minus_mod_eq_div2 ~> minus_mod_eq_mult_div 

453 
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] 

454 
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] 

455 
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] 

456 
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] 

457 
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

458 
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

459 
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

460 
div_1 ~> div_by_Suc_0 

461 
mod_1 ~> mod_by_Suc_0 

462 
INCOMPATIBILITY. 

463 

464 
* New type class "idom_abs_sgn" specifies algebraic properties 

465 
of sign and absolute value functions. Type class "sgn_if" has 

466 
disappeared. Slight INCOMPATIBILITY. 

467 

468 
* Dedicated syntax LENGTH('a) for length of types. 

469 

63977  470 
* Characters (type char) are modelled as finite algebraic type 
471 
corresponding to {0..255}. 

472 

473 
 Logical representation: 

474 
* 0 is instantiated to the ASCII zero character. 

475 
* All other characters are represented as "Char n" 

476 
with n being a raw numeral expression less than 256. 

477 
* Expressions of the form "Char n" with n greater than 255 

478 
are noncanonical. 

479 
 Printing and parsing: 

480 
* Printable characters are printed and parsed as "CHR ''\<dots>''" 

481 
(as before). 

482 
* The ASCII zero character is printed and parsed as "0". 

483 
* All other canonical characters are printed as "CHR 0xXX" 

484 
with XX being the hexadecimal character code. "CHR n" 

485 
is parsable for every numeral expression n. 

486 
* Noncanonical characters have no special syntax and are 

487 
printed as their logical representation. 

488 
 Explicit conversions from and to the natural numbers are 

489 
provided as char_of_nat, nat_of_char (as before). 

490 
 The auxiliary nibble type has been discontinued. 

491 

492 
INCOMPATIBILITY. 

493 

494 
* Type class "div" with operation "mod" renamed to type class "modulo" 

495 
with operation "modulo", analogously to type class "divide". This 

496 
eliminates the need to qualify any of those names in the presence of 

497 
infix "mod" syntax. INCOMPATIBILITY. 

498 

63979  499 
* Statements and proofs of KnasterTarski fixpoint combinators lfp/gfp 
500 
have been clarified. The fixpoint properties are lfp_fixpoint, its 

501 
symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items 

502 
for the proof (lfp_lemma2 etc.) are no longer exported, but can be 

503 
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY. 

504 

63977  505 
* Constant "surj" is a mere input abbreviation, to avoid hiding an 
506 
equation in term output. Minor INCOMPATIBILITY. 

507 

508 
* Command 'code_reflect' accepts empty constructor lists for datatypes, 

509 
which renders those abstract effectively. 

510 

511 
* Command 'export_code' checks given constants for abstraction 

512 
violations: a small guarantee that given constants specify a safe 

513 
interface for the generated code. 

514 

515 
* Code generation for Scala: ambiguous implicts in class diagrams are 

516 
spelt out explicitly. 

517 

518 
* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on 

519 
explicitly provided auxiliary definitions for required type class 

64390  520 
dictionaries rather than halfworking magic. INCOMPATIBILITY, see the 
521 
tutorial on code generation for details. 

522 

523 
* Theory Set_Interval: substantial new theorems on indexed sums and 

524 
products. 

63977  525 

526 
* Locale bijection establishes convenient default simp rules such as 

527 
"inv f (f a) = a" for total bijections. 

528 

529 
* Abstract locales semigroup, abel_semigroup, semilattice, 

530 
semilattice_neutr, ordering, ordering_top, semilattice_order, 

531 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 

532 
semilattice_neutr_set, semilattice_order_set, 

533 
semilattice_order_neutr_set monoid_list, comm_monoid_list, 

534 
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified 

535 
syntax uniformly that does not clash with corresponding global syntax. 

536 
INCOMPATIBILITY. 

537 

538 
* Former locale lifting_syntax is now a bundle, which is easier to 

539 
include in a local context or theorem statement, e.g. "context includes 

540 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

541 

63807  542 
* Some old / obsolete theorems have been renamed / removed, potential 
543 
INCOMPATIBILITY. 

544 

545 
nat_less_cases  removed, use linorder_cases instead 

546 
inv_image_comp  removed, use image_inv_f_f instead 

547 
image_surj_f_inv_f ~> image_f_inv_f 

63113  548 

63456
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

549 
* Some theorems about groups and orders have been generalised from 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

550 
groups to semigroups that are also monoids: 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

551 
le_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

552 
le_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

553 
less_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

554 
less_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

555 
add_le_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

556 
add_le_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

557 
add_less_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

558 
add_less_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

559 

3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

560 
* Some simplifications theorems about rings have been removed, since 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

561 
superseeded by a more general version: 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

562 
less_add_cancel_left_greater_zero ~> less_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

563 
less_add_cancel_right_greater_zero ~> less_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

564 
less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

565 
less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

566 
less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

567 
less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

568 
less_add_cancel_left_less_zero ~> add_less_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

569 
less_add_cancel_right_less_zero ~> add_less_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

570 
INCOMPATIBILITY. 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

571 

62407  572 
* Renamed split_if > if_split and split_if_asm > if_split_asm to 
573 
resemble the f.split naming convention, INCOMPATIBILITY. 

62396  574 

63977  575 
* Added class topological_monoid. 
576 

64391  577 
* The following theorems have been renamed: 
578 

64457  579 
setsum_left_distrib ~> sum_distrib_right 
580 
setsum_right_distrib ~> sum_distrib_left 

64391  581 

582 
INCOMPATIBILITY. 

583 

584 
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. 

585 
INCOMPATIBILITY. 

586 

587 
* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional 

588 
comprehensionlike syntax analogously to "Inf (f ` A)" and "Sup (f ` 

589 
A)". 

590 

591 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 

592 

593 
* The type class ordered_comm_monoid_add is now called 

594 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 

595 
is introduced as the combination of ordered_ab_semigroup_add + 

596 
comm_monoid_add. INCOMPATIBILITY. 

597 

598 
* Introduced the type classes canonically_ordered_comm_monoid_add and 

599 
dioid. 

600 

601 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 

602 
instantiating linordered_semiring_strict and ordered_ab_group_add, an 

603 
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 

604 
be required. INCOMPATIBILITY. 

63117  605 

62348  606 
* Dropped various legacy fact bindings, whose replacements are often 
607 
of a more general type also: 

608 
lcm_left_commute_nat ~> lcm.left_commute 

609 
lcm_left_commute_int ~> lcm.left_commute 

610 
gcd_left_commute_nat ~> gcd.left_commute 

611 
gcd_left_commute_int ~> gcd.left_commute 

612 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

613 
gcd_greatest_iff_int ~> gcd_greatest_iff 

614 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

615 
coprime_dvd_mult_int ~> coprime_dvd_mult 

616 
zpower_numeral_even ~> power_numeral_even 

617 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

618 
gcd_mult_cancel_int ~> gcd_mult_cancel 

619 
div_gcd_coprime_nat ~> div_gcd_coprime 

620 
div_gcd_coprime_int ~> div_gcd_coprime 

621 
zpower_numeral_odd ~> power_numeral_odd 

622 
zero_less_int_conv ~> of_nat_0_less_iff 

623 
gcd_greatest_nat ~> gcd_greatest 

624 
gcd_greatest_int ~> gcd_greatest 

625 
coprime_mult_nat ~> coprime_mult 

626 
coprime_mult_int ~> coprime_mult 

627 
lcm_commute_nat ~> lcm.commute 

628 
lcm_commute_int ~> lcm.commute 

629 
int_less_0_conv ~> of_nat_less_0_iff 

630 
gcd_commute_nat ~> gcd.commute 

631 
gcd_commute_int ~> gcd.commute 

632 
Gcd_insert_nat ~> Gcd_insert 

633 
Gcd_insert_int ~> Gcd_insert 

634 
of_int_int_eq ~> of_int_of_nat_eq 

635 
lcm_least_nat ~> lcm_least 

636 
lcm_least_int ~> lcm_least 

637 
lcm_assoc_nat ~> lcm.assoc 

638 
lcm_assoc_int ~> lcm.assoc 

639 
int_le_0_conv ~> of_nat_le_0_iff 

640 
int_eq_0_conv ~> of_nat_eq_0_iff 

641 
Gcd_empty_nat ~> Gcd_empty 

642 
Gcd_empty_int ~> Gcd_empty 

643 
gcd_assoc_nat ~> gcd.assoc 

644 
gcd_assoc_int ~> gcd.assoc 

645 
zero_zle_int ~> of_nat_0_le_iff 

646 
lcm_dvd2_nat ~> dvd_lcm2 

647 
lcm_dvd2_int ~> dvd_lcm2 

648 
lcm_dvd1_nat ~> dvd_lcm1 

649 
lcm_dvd1_int ~> dvd_lcm1 

650 
gcd_zero_nat ~> gcd_eq_0_iff 

651 
gcd_zero_int ~> gcd_eq_0_iff 

652 
gcd_dvd2_nat ~> gcd_dvd2 

653 
gcd_dvd2_int ~> gcd_dvd2 

654 
gcd_dvd1_nat ~> gcd_dvd1 

655 
gcd_dvd1_int ~> gcd_dvd1 

656 
int_numeral ~> of_nat_numeral 

657 
lcm_ac_nat ~> ac_simps 

658 
lcm_ac_int ~> ac_simps 

659 
gcd_ac_nat ~> ac_simps 

660 
gcd_ac_int ~> ac_simps 

661 
abs_int_eq ~> abs_of_nat 

662 
zless_int ~> of_nat_less_iff 

663 
zdiff_int ~> of_nat_diff 

664 
zadd_int ~> of_nat_add 

665 
int_mult ~> of_nat_mult 

666 
int_Suc ~> of_nat_Suc 

667 
inj_int ~> inj_of_nat 

668 
int_1 ~> of_nat_1 

669 
int_0 ~> of_nat_0 

62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

670 
Lcm_empty_nat ~> Lcm_empty 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

671 
Lcm_empty_int ~> Lcm_empty 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

672 
Lcm_insert_nat ~> Lcm_insert 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

673 
Lcm_insert_int ~> Lcm_insert 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

674 
comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

675 
comp_fun_idem_gcd_int ~> comp_fun_idem_gcd 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

676 
comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

677 
comp_fun_idem_lcm_int ~> comp_fun_idem_lcm 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

678 
Lcm_eq_0 ~> Lcm_eq_0_I 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

679 
Lcm0_iff ~> Lcm_0_iff 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

680 
Lcm_dvd_int ~> Lcm_least 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

681 
divides_mult_nat ~> divides_mult 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

682 
divides_mult_int ~> divides_mult 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

683 
lcm_0_nat ~> lcm_0_right 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

684 
lcm_0_int ~> lcm_0_right 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

685 
lcm_0_left_nat ~> lcm_0_left 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

686 
lcm_0_left_int ~> lcm_0_left 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

687 
dvd_gcd_D1_nat ~> dvd_gcdD1 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

688 
dvd_gcd_D1_int ~> dvd_gcdD1 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

689 
dvd_gcd_D2_nat ~> dvd_gcdD2 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

690 
dvd_gcd_D2_int ~> dvd_gcdD2 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

691 
coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

692 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  693 
realpow_minus_mult ~> power_minus_mult 
694 
realpow_Suc_le_self ~> power_Suc_le_self 

62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

695 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  696 
INCOMPATIBILITY. 
697 

63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset

698 
* Renamed HOL/Quotient_Examples/FSet.thy to 
63977  699 
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. 
700 

64390  701 
* Session HOLLibrary: theory FinFun bundles "finfun_syntax" and 
702 
"no_finfun_syntax" allow to control optional syntax in local contexts; 

703 
this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use 

704 
"unbundle finfun_syntax" to imitate import of 

705 
"~~/src/HOL/Library/FinFun_Syntax". 

706 

707 
* Session HOLLibrary: theory Multiset_Permutations (executably) defines 

708 
the set of permutations of a given set or multiset, i.e. the set of all 

709 
lists that contain every element of the carrier (multi)set exactly 

710 
once. 

711 

712 
* Session HOLLibrary: multiset membership is now expressed using 

713 
set_mset rather than count. 

714 

715 
 Expressions "count M a > 0" and similar simplify to membership 

716 
by default. 

717 

718 
 Converting between "count M a = 0" and nonmembership happens using 

719 
equations count_eq_zero_iff and not_in_iff. 

720 

721 
 Rules count_inI and in_countE obtain facts of the form 

722 
"count M a = n" from membership. 

723 

724 
 Rules count_in_diffI and in_diff_countE obtain facts of the form 

725 
"count M a = n + count N a" from membership on difference sets. 

726 

727 
INCOMPATIBILITY. 

728 

729 
* Session HOLLibrary: theory LaTeXsugar uses newstyle "dummy_pats" for 

730 
displaying equations in functional programming style  variables 

731 
present on the lefthand but not on the righhand side are replaced by 

732 
underscores. 

733 

734 
* Session HOLLibrary: theory Combinator_PER provides combinator to 

735 
build partial equivalence relations from a predicate and an equivalence 

736 
relation. 

737 

738 
* Session HOLLibrary: theory Perm provides basic facts about almost 

739 
everywhere fix bijections. 

740 

741 
* Session HOLLibrary: theory Normalized_Fraction allows viewing an 

742 
element of a field of fractions as a normalized fraction (i.e. a pair of 

743 
numerator and denominator such that the two are coprime and the 

744 
denominator is normalized wrt. unit factors). 

745 

746 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 

747 

748 
* Session HOLMultivariate_Analysis has been renamed to HOLAnalysis. 

749 

750 
* Session HOLAnalysis: measure theory has been moved here from 

751 
HOLProbability. When importing HOLAnalysis some theorems need 

752 
additional name spaces prefixes due to name clashes. INCOMPATIBILITY. 

753 

754 
* Session HOLAnalysis: more complex analysis including Cauchy's 

755 
inequality, Liouville theorem, open mapping theorem, maximum modulus 

756 
principle, Residue theorem, Schwarz Lemma. 

757 

758 
* Session HOLAnalysis: Theory of polyhedra: faces, extreme points, 

759 
polytopes, and the Kreinâ€“Milman Minkowski theorem. 

760 

761 
* Session HOLAnalysis: Numerous results ported from the HOL Light 

762 
libraries: homeomorphisms, continuous function extensions, invariance of 

763 
domain. 

764 

765 
* Session HOLProbability: the type of emeasure and nn_integral was 

766 
changed from ereal to ennreal, INCOMPATIBILITY. 

767 

768 
emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal 

769 
nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal 

770 

771 
* Session HOLProbability: Code generation and QuickCheck for 

772 
Probability Mass Functions. 

773 

774 
* Session HOLProbability: theory Random_Permutations contains some 

775 
theory about choosing a permutation of a set uniformly at random and 

776 
folding over a list in random order. 

777 

778 
* Session HOLProbability: theory SPMF formalises discrete 

779 
subprobability distributions. 

780 

781 
* Session HOLLibrary: the names of multiset theorems have been 

782 
normalised to distinguish which ordering the theorems are about 

783 

784 
mset_less_eqI ~> mset_subset_eqI 

785 
mset_less_insertD ~> mset_subset_insertD 

786 
mset_less_eq_count ~> mset_subset_eq_count 

787 
mset_less_diff_self ~> mset_subset_diff_self 

788 
mset_le_exists_conv ~> mset_subset_eq_exists_conv 

789 
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel 

790 
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel 

791 
mset_le_mono_add ~> mset_subset_eq_mono_add 

792 
mset_le_add_left ~> mset_subset_eq_add_left 

793 
mset_le_add_right ~> mset_subset_eq_add_right 

794 
mset_le_single ~> mset_subset_eq_single 

795 
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute 

796 
diff_le_self ~> diff_subset_eq_self 

797 
mset_leD ~> mset_subset_eqD 

798 
mset_lessD ~> mset_subsetD 

799 
mset_le_insertD ~> mset_subset_eq_insertD 

800 
mset_less_of_empty ~> mset_subset_of_empty 

801 
mset_less_size ~> mset_subset_size 

802 
wf_less_mset_rel ~> wf_subset_mset_rel 

803 
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq 

804 
mset_remdups_le ~> mset_remdups_subset_eq 

805 
ms_lesseq_impl ~> subset_eq_mset_impl 

806 

807 
Some functions have been renamed: 

808 
ms_lesseq_impl > subset_eq_mset_impl 

809 

810 
* HOLLibrary: multisets are now ordered with the multiset ordering 

811 
#\<subseteq># ~> \<le> 

812 
#\<subset># ~> < 

813 
le_multiset ~> less_eq_multiset 

814 
less_multiset ~> le_multiset 

815 
INCOMPATIBILITY. 

816 

817 
* Session HOLLibrary: the prefix multiset_order has been discontinued: 

818 
the theorems can be directly accessed. As a consequence, the lemmas 

819 
"order_multiset" and "linorder_multiset" have been discontinued, and the 

820 
interpretations "multiset_linorder" and "multiset_wellorder" have been 

821 
replaced by instantiations. INCOMPATIBILITY. 

822 

823 
* Session HOLLibrary: some theorems about the multiset ordering have 

824 
been renamed: 

825 

826 
le_multiset_def ~> less_eq_multiset_def 

827 
less_multiset_def ~> le_multiset_def 

828 
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset 

829 
mult_less_not_refl ~> mset_le_not_refl 

830 
mult_less_trans ~> mset_le_trans 

831 
mult_less_not_sym ~> mset_le_not_sym 

832 
mult_less_asym ~> mset_le_asym 

833 
mult_less_irrefl ~> mset_le_irrefl 

834 
union_less_mono2{,1,2} ~> union_le_mono2{,1,2} 

835 

836 
le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O 

837 
le_multiset_total ~> less_eq_multiset_total 

838 
less_multiset_right_total ~> subset_eq_imp_le_multiset 

839 
le_multiset_empty_left ~> less_eq_multiset_empty_left 

840 
le_multiset_empty_right ~> less_eq_multiset_empty_right 

841 
less_multiset_empty_right ~> le_multiset_empty_left 

842 
less_multiset_empty_left ~> le_multiset_empty_right 

843 
union_less_diff_plus ~> union_le_diff_plus 

844 
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset 

845 
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty 

846 
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty 

847 
INCOMPATIBILITY. 

848 

849 
* Session HOLLibrary: the lemma mset_map has now the attribute [simp]. 

850 
INCOMPATIBILITY. 

851 

852 
* Session HOLLibrary: some theorems about multisets have been removed. 

853 
INCOMPATIBILITY, use the following replacements: 

854 

855 
le_multiset_plus_plus_left_iff ~> add_less_cancel_right 

856 
less_multiset_plus_plus_left_iff ~> add_less_cancel_right 

857 
le_multiset_plus_plus_right_iff ~> add_less_cancel_left 

858 
less_multiset_plus_plus_right_iff ~> add_less_cancel_left 

859 
add_eq_self_empty_iff ~> add_cancel_left_right 

860 
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right 

861 
mset_less_add_bothsides ~> subset_mset.add_less_cancel_right 

862 
mset_le_add_bothsides ~> subset_mset.add_less_cancel_right 

863 
empty_inter ~> subset_mset.inf_bot_left 

864 
inter_empty ~> subset_mset.inf_bot_right 

865 
empty_sup ~> subset_mset.sup_bot_left 

866 
sup_empty ~> subset_mset.sup_bot_right 

867 
bdd_below_multiset ~> subset_mset.bdd_above_bot 

868 
subset_eq_empty ~> subset_mset.le_zero_eq 

869 
le_empty ~> subset_mset.le_zero_eq 

870 
mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

871 
mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

872 

873 
* Session HOLLibrary: some typeclass constraints about multisets have 

874 
been reduced from ordered or linordered to preorder. Multisets have the 

875 
additional typeclasses order_bot, no_top, 

876 
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, 

877 
linordered_cancel_ab_semigroup_add, and 

878 
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. 

879 

880 
* Session HOLLibrary: there are some new simplification rules about 

881 
multisets, the multiset ordering, and the subset ordering on multisets. 

882 
INCOMPATIBILITY. 

883 

884 
* Session HOLLibrary: the subset ordering on multisets has now the 

885 
interpretations ordered_ab_semigroup_monoid_add_imp_le and 

886 
bounded_lattice_bot. INCOMPATIBILITY. 

887 

888 
* Session HOLLibrary, theory Multiset: single has been removed in favor 

889 
of add_mset that roughly corresponds to Set.insert. Some theorems have 

890 
removed or changed: 

891 

892 
single_not_empty ~> add_mset_not_empty or empty_not_add_mset 

893 
fold_mset_insert ~> fold_mset_add_mset 

894 
image_mset_insert ~> image_mset_add_mset 

895 
union_single_eq_diff 

896 
multi_self_add_other_not_self 

897 
diff_single_eq_union 

898 
INCOMPATIBILITY. 

899 

900 
* Session HOLLibrary, theory Multiset: some theorems have been changed 

901 
to use add_mset instead of single: 

902 

903 
mset_add 

904 
multi_self_add_other_not_self 

905 
diff_single_eq_union 

906 
union_single_eq_diff 

907 
union_single_eq_member 

908 
add_eq_conv_diff 

909 
insert_noteq_member 

910 
add_eq_conv_ex 

911 
multi_member_split 

912 
multiset_add_sub_el_shuffle 

913 
mset_subset_eq_insertD 

914 
mset_subset_insertD 

915 
insert_subset_eq_iff 

916 
insert_union_subset_iff 

917 
multi_psub_of_add_self 

918 
inter_add_left1 

919 
inter_add_left2 

920 
inter_add_right1 

921 
inter_add_right2 

922 
sup_union_left1 

923 
sup_union_left2 

924 
sup_union_right1 

925 
sup_union_right2 

926 
size_eq_Suc_imp_eq_union 

927 
multi_nonempty_split 

928 
mset_insort 

929 
mset_update 

930 
mult1I 

931 
less_add 

932 
mset_zip_take_Cons_drop_twice 

933 
rel_mset_Zero 

934 
msed_map_invL 

935 
msed_map_invR 

936 
msed_rel_invL 

937 
msed_rel_invR 

938 
le_multiset_right_total 

939 
multiset_induct 

940 
multiset_induct2_size 

941 
multiset_induct2 

942 
INCOMPATIBILITY. 

943 

944 
* Session HOLLibrary, theory Multiset: the definitions of some 

945 
constants have changed to use add_mset instead of adding a single 

946 
element: 

947 

948 
image_mset 

949 
mset 

950 
replicate_mset 

951 
mult1 

952 
pred_mset 

953 
rel_mset' 

954 
mset_insort 

955 

956 
INCOMPATIBILITY. 

957 

958 
* Session HOLLibrary, theory Multiset: due to the above changes, the 

959 
attributes of some multiset theorems have been changed: 

960 

961 
insert_DiffM [] ~> [simp] 

962 
insert_DiffM2 [simp] ~> [] 

963 
diff_add_mset_swap [simp] 

964 
fold_mset_add_mset [simp] 

965 
diff_diff_add [simp] (for multisets only) 

966 
diff_cancel [simp] ~> [] 

967 
count_single [simp] ~> [] 

968 
set_mset_single [simp] ~> [] 

969 
size_multiset_single [simp] ~> [] 

970 
size_single [simp] ~> [] 

971 
image_mset_single [simp] ~> [] 

972 
mset_subset_eq_mono_add_right_cancel [simp] ~> [] 

973 
mset_subset_eq_mono_add_left_cancel [simp] ~> [] 

974 
fold_mset_single [simp] ~> [] 

975 
subset_eq_empty [simp] ~> [] 

976 
empty_sup [simp] ~> [] 

977 
sup_empty [simp] ~> [] 

978 
inter_empty [simp] ~> [] 

979 
empty_inter [simp] ~> [] 

980 
INCOMPATIBILITY. 

981 

64391  982 
* Session HOLLibrary, theory Multiset: the order of the variables in 
64390  983 
the second cases of multiset_induct, multiset_induct2_size, 
984 
multiset_induct2 has been changed (e.g. Add A a ~> Add a A). 

985 
INCOMPATIBILITY. 

986 

987 
* Session HOLLibrary, theory Multiset: there is now a simplification 

988 
procedure on multisets. It mimics the behavior of the procedure on 

989 
natural numbers. INCOMPATIBILITY. 

990 

991 
* Session HOLLibrary, theory Multiset: renamed sums and products of 

992 
multisets: 

993 

994 
msetsum ~> sum_mset 

995 
msetprod ~> prod_mset 

996 

997 
* Session HOLLibrary, theory Multiset: the notation for intersection 

998 
and union of multisets have been changed: 

999 

1000 
#\<inter> ~> \<inter># 

1001 
#\<union> ~> \<union># 

1002 

1003 
INCOMPATIBILITY. 

1004 

1005 
* Session HOLLibrary, theory Multiset: the lemma 

1006 
one_step_implies_mult_aux on multisets has been removed, use 

1007 
one_step_implies_mult instead. INCOMPATIBILITY. 

1008 

1009 
* Session HOLLibrary: theory Complete_Partial_Order2 provides reasoning 

1010 
support for monotonicity and continuity in chaincomplete partial orders 

1011 
and about admissibility conditions for fixpoint inductions. 

1012 

64523  1013 
* Session HOLLibrary: theory Library/Polynomial contains also 
1014 
derivation of polynomials (formerly in Library/Poly_Deriv) but not 

1015 
gcd/lcm on polynomials over fields. This has been moved to a separate 

1016 
theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible 

1017 
future different type class instantiation for polynomials over factorial 

1018 
rings. INCOMPATIBILITY. 

64390  1019 

1020 
* Session HOLLibrary: theory Sublist provides function "prefixes" with 

1021 
the following renaming 

1022 

1023 
prefixeq > prefix 

1024 
prefix > strict_prefix 

1025 
suffixeq > suffix 

1026 
suffix > strict_suffix 

1027 

1028 
Added theory of longest common prefixes. 

64389  1029 

64391  1030 
* Session HOLNumber_Theory: algebraic foundation for primes: 
1031 
Generalisation of predicate "prime" and introduction of predicates 

1032 
"prime_elem", "irreducible", a "prime_factorization" function, and the 

1033 
"factorial_ring" typeclass with instance proofs for nat, int, poly. Some 

1034 
theorems now have different names, most notably "prime_def" is now 

1035 
"prime_nat_iff". INCOMPATIBILITY. 

1036 

1037 
* Session Old_Number_Theory has been removed, after porting remaining 

1038 
theories. 

1039 

64551  1040 
* Session HOLTypes_To_Sets provides an experimental extension of 
1041 
HigherOrder Logic to allow translation of types to sets. 

1042 

63198
c583ca33076a
adhoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63184
diff
changeset

1043 

62498  1044 
*** ML *** 
1045 

63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63226
diff
changeset

1046 
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML 
63228  1047 
library (notably for big integers). Subtle change of semantics: 
1048 
Integer.gcd and Integer.lcm both normalize the sign, results are never 

1049 
negative. This coincides with the definitions in HOL/GCD.thy. 

1050 
INCOMPATIBILITY. 

63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63226
diff
changeset

1051 

63212  1052 
* Structure Rat for rational numbers is now an integral part of 
63215  1053 
Isabelle/ML, with special notation @int/nat or @int for numerals (an 
1054 
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty 

63212  1055 
printing. Standard operations on type Rat.rat are provided via adhoc 
63215  1056 
overloading of +  * / < <= > >= ~ abs. INCOMPATIBILITY, need to 
63212  1057 
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been 
1058 
superseded by General.Div. 

63198
c583ca33076a
adhoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63184
diff
changeset

1059 

64390  1060 
* ML antiquotation @{path} is superseded by @{file}, which ensures that 
1061 
the argument is a plain file. Minor INCOMPATIBILITY. 

1062 

1063 
* Antiquotation @{make_string} is available during Pure bootstrap  

1064 
with approximative output quality. 

1065 

1066 
* Lowlevel ML system structures (like PolyML and RunCall) are no longer 

1067 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 

1068 

62861  1069 
* The ML function "ML" provides easy access to runtime compilation. 
1070 
This is particularly useful for conditional compilation, without 

1071 
requiring separate files. 

1072 

62498  1073 
* Option ML_exception_debugger controls detailed exception trace via the 
1074 
Poly/ML debugger. Relevant ML modules need to be compiled beforehand 

1075 
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note 

1076 
debugger information requires consirable time and space: main 

1077 
Isabelle/HOL with full debugger support may need ML_system_64. 

1078 

62514  1079 
* Local_Theory.restore has been renamed to Local_Theory.reset to 
1080 
emphasize its disruptive impact on the cumulative context, notably the 

1081 
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is 

1082 
only appropriate when targets are managed, e.g. starting from a global 

1083 
theory and returning to it. Regular definitional packages should use 

1084 
balanced blocks of Local_Theory.open_target versus 

1085 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

1086 

62519  1087 
* Structure TimeLimit (originally from the SML/NJ library) has been 
1088 
replaced by structure Timeout, with slightly different signature. 

1089 
INCOMPATIBILITY. 

1090 

62551  1091 
* Discontinued cd and pwd operations, which are not welldefined in a 
1092 
multithreaded environment. Note that files are usually located 

1093 
relatively to the master directory of a theory (see also 

1094 
File.full_path). Potential INCOMPATIBILITY. 

1095 

63352  1096 
* Binding.empty_atts supersedes Thm.empty_binding and 
1097 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

1098 

62498  1099 

62354  1100 
*** System *** 
1101 

64390  1102 
* SML/NJ and old versions of Poly/ML are no longer supported. 
1103 

1104 
* Poly/ML heaps now follow the hierarchy of sessions, and thus require 

1105 
much less disk space. 

63226  1106 

62591  1107 
* The Isabelle ML process is now managed directly by Isabelle/Scala, and 
1108 
shell scripts merely provide optional commandline access. In 

1109 
particular: 

1110 

1111 
. Scala module ML_Process to connect to the raw ML process, 

1112 
with interaction via stdin/stdout/stderr or in batch mode; 

1113 
. commandline tool "isabelle console" as interactive wrapper; 

1114 
. commandline tool "isabelle process" as batch mode wrapper. 

62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1115 

cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1116 
* The executable "isabelle_process" has been discontinued. Tools and 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1117 
prover frontends should use ML_Process or Isabelle_Process in 
62591  1118 
Isabelle/Scala. INCOMPATIBILITY. 
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1119 

cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1120 
* New commandline tool "isabelle process" supports ML evaluation of 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1121 
literal expressions (option e) or files (option f) in the context of a 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1122 
given heap image. Errors lead to premature exit of the ML process with 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1123 
return code 1. 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1124 

64390  1125 
* The commandline tool "isabelle build" supports option N for cyclic 
1126 
shuffling of NUMA CPU nodes. This may help performance tuning on Linux 

1127 
servers with separate CPU/memory modules. 

1128 

1129 
* System option "threads" (for the size of the Isabelle/ML thread farm) 

1130 
is also passed to the underlying ML runtime system as gcthreads, 

64274  1131 
unless there is already a default provided via ML_OPTIONS settings. 
1132 

63827
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1133 
* System option "checkpoint" helps to finetune the global heap space 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1134 
management of isabelle build. This is relevant for big sessions that may 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1135 
exhaust the small 32bit address space of the ML process (which is used 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1136 
by default). 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1137 

64308  1138 
* System option "profiling" specifies the mode for global ML profiling 
64342  1139 
in "isabelle build". Possible values are "time", "allocations". The 
1140 
commandline tool "isabelle profiling_report" helps to digest the 

1141 
resulting log files. 

64308  1142 

63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63979
diff
changeset

1143 
* System option "ML_process_policy" specifies an optional command prefix 
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63979
diff
changeset

1144 
for the underlying ML process, e.g. to control CPU affinity on 
63987
ac96fe9224f6
just one option is enough  "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents:
63986
diff
changeset

1145 
multiprocessor systems. The "isabelle jedit" tool allows to override the 
ac96fe9224f6
just one option is enough  "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents:
63986
diff
changeset

1146 
implicit default via option p. 
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63979
diff
changeset

1147 

64390  1148 
* Commandline tool "isabelle console" provides option r to help to 
1149 
bootstrapping Isabelle/Pure interactively. 

1150 

1151 
* Commandline tool "isabelle yxml" has been discontinued. 

1152 
INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in 

1153 
Isabelle/ML or Isabelle/Scala. 

1154 

1155 
* Many Isabelle tools that require a Java runtime system refer to the 

1156 
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, 

1157 
depending on the underlying platform. The settings for "isabelle build" 

1158 
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been 

1159 
discontinued. Potential INCOMPATIBILITY. 

1160 

1161 
* The Isabelle system environment always ensures that the main 

1162 
executables are found within the shell search $PATH: "isabelle" and 

1163 
"isabelle_scala_script". 

1164 

1165 
* Isabelle tools may consist of .scala files: the Scala compiler is 

1166 
invoked on the spot. The source needs to define some object that extends 

1167 
Isabelle_Tool.Body. 

1168 

1169 
* File.bash_string, File.bash_path etc. represent Isabelle/ML and 

1170 
Isabelle/Scala strings authentically within GNU bash. This is useful to 

1171 
produce robust shell scripts under program control, without worrying 

1172 
about spaces or special characters. Note that user output works via 

1173 
Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and 

1174 
less versatile) operations File.shell_quote, File.shell_path etc. have 

1175 
been discontinued. 

1176 

63995  1177 
* The isabelle_java executable allows to run a Java process within the 
1178 
name space of Java and Scala components that are bundled with Isabelle, 

1179 
but without the Isabelle settings environment. 

1180 

64390  1181 
* Isabelle/Scala: the SSH module supports ssh and sftp connections, for 
1182 
remote commandexecution and filesystem access. This resembles 

1183 
operations from module File and Isabelle_System to some extent. Note 

1184 
that Path specifications need to be resolved remotely via 

1185 
ssh.remote_path instead of File.standard_path: the implicit process 

1186 
environment is different, Isabelle settings are not available remotely. 

1187 

1188 
* Isabelle/Scala: the Mercurial module supports repositories via the 

1189 
regular hg commandline interface. The repositroy clone and working 

1190 
directory may reside on a local or remote filesystem (via ssh 

1191 
connection). 

64265  1192 

62354  1193 

1194 

62031  1195 
New in Isabelle2016 (February 2016) 
62016  1196 
 
60138  1197 

61337  1198 
*** General *** 
1199 

62168
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

1200 
* Eisbach is now based on Pure instead of HOL. Objectslogics may import 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

1201 
either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

1202 
~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

1203 
the HOLEisbach session located in ~~/src/HOL/Eisbach/ contains further 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

1204 
examples that do require HOL. 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

1205 

62157  1206 
* Better resource usage on all platforms (Linux, Windows, Mac OS X) for 
1207 
both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage. 

1208 

62017  1209 
* Former "xsymbols" syntax with Isabelle symbols is used by default, 
1210 
without any special print mode. Important ASCII replacement syntax 

1211 
remains available under print mode "ASCII", but less important syntax 

1212 
has been removed (see below). 

1213 

62109  1214 
* Support for more arrow symbols, with rendering in LaTeX and Isabelle 
1215 
fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>. 

62017  1216 

62108
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1217 
* Special notation \<struct> for the first implicit 'structure' in the 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1218 
context has been discontinued. Rare INCOMPATIBILITY, use explicit 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1219 
structure name instead, notably in indexed notation with blocksubscript 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1220 
(e.g. \<odot>\<^bsub>A\<^esub>). 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1221 

0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1222 
* The glyph for \<diamond> in the IsabelleText font now corresponds better to its 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1223 
counterpart \<box> as quantifierlike symbol. A small diamond is available as 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1224 
\<diamondop>; the old symbol \<struct> loses this rendering and any special 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1225 
meaning. 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

1226 

62017  1227 
* Syntax for formal comments " text" now also supports the symbolic 
1228 
form "\<comment> text". Commandline tool "isabelle update_cartouches c" helps 

1229 
to update old sources. 

1230 

61337  1231 
* Toplevel theorem statements have been simplified as follows: 
1232 

1233 
theorems ~> lemmas 

1234 
schematic_lemma ~> schematic_goal 

1235 
schematic_theorem ~> schematic_goal 

1236 
schematic_corollary ~> schematic_goal 

1237 

1238 
Commandline tool "isabelle update_theorems" updates theory sources 

1239 
accordingly. 

1240 

61338  1241 
* Toplevel theorem statement 'proposition' is another alias for 
1242 
'theorem'. 

1243 

62169  1244 
* The old 'defs' command has been removed (legacy since Isabelle2014). 
1245 
INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or 

1246 
deferred definitions require a surrounding 'overloading' block. 

1247 

61337  1248 

60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset

1249 
*** Prover IDE  Isabelle/Scala/jEdit *** 
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset

1250 

60986  1251 
* IDE support for the sourcelevel debugger of Poly/ML, to work with 
62253  1252 
Isabelle/ML and official Standard ML. Option "ML_debugger" and commands 
1253 
'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', 

1254 
'SML_file_no_debug' control compilation of sources with or without 

1255 
debugging information. The Debugger panel allows to set breakpoints (via 

1256 
context menu), step through stopped threads, evaluate local ML 

1257 
expressions etc. At least one Debugger view needs to be active to have 

1258 
any effect on the running ML program. 

60984  1259 

61803  1260 
* The State panel manages explicit proof state output, with dynamic 
1261 
autoupdate according to cursor movement. Alternatively, the jEdit 

1262 
action "isabelle.updatestate" (shortcut S+ENTER) triggers manual 

1263 
update. 

61729  1264 

1265 
* The Output panel no longer shows proof state output by default, to 

1266 
avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or 

1267 
enable option "editor_output_state". 

61215  1268 

61803  1269 
* The text overview column (status of errors, warnings etc.) is updated 
1270 
asynchronously, leading to much better editor reactivity. Moreover, the 

1271 
full document node content is taken into account. The width of the 

1272 
column is scaled according to the main text area font, for improved 

1273 
visibility. 

1274 

1275 
* The main text area no longer changes its color hue in outdated 

1276 
situations. The text overview column takes over the role to indicate 

1277 
unfinished edits in the PIDE pipeline. This avoids flashing text display 

1278 
due to adhoc updates by auxiliary GUI components, such as the State 

1279 
panel. 

1280 

62254
81cbea2babd9
tuned NEWS: longrunning tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset

1281 
* Slightly improved scheduling for urgent print tasks (e.g. command 
81cbea2babd9
tuned NEWS: longrunning tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset

1282 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1283 

1284 
* Completion of symbols via prefix of \<name> or \<^name> or \name is 

1285 
always possible, independently of the language context. It is never 

1286 
implicit: a popup will show up unconditionally. 

1287 

1288 
* Additional abbreviations for syntactic completion may be specified in 

1289 
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with 

1290 
support for simple templates using ASCII 007 (bell) as placeholder. 

1291 

62234
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

1292 
* Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

1293 
completion like "+o", "*o", ".o" etc.  due to conflicts with other 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

1294 
ASCII syntax. INCOMPATIBILITY, use plain backslashcompletion or define 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

1295 
suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs. 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

1296 

61483  1297 
* Action "isabelleemph" (with keyboard shortcut C+e LEFT) controls 
1298 
emphasized text style; the effect is visible in document output, not in 

1299 
the editor. 

1300 

1301 
* Action "isabellereset" now uses keyboard shortcut C+e BACK_SPACE, 

1302 
instead of former C+e LEFT. 

1303 

61512
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

1304 
* The commandline tool "isabelle jedit" and the isabelle.Main 
62027  1305 
application wrapper treat the default $USER_HOME/Scratch.thy more 
61512
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

1306 
uniformly, and allow the dummy file argument ":" to open an empty buffer 
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

1307 
instead. 
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

1308 

62017  1309 
* New commandline tool "isabelle jedit_client" allows to connect to an 
1310 
already running Isabelle/jEdit process. This achieves the effect of 

1311 
singleinstance applications seen on common GUI desktops. 

1312 

61529
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset

1313 
* The default lookandfeel for Linux is the traditional "Metal", which 
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset

1314 
works better with GUI scaling for very highresolution displays (e.g. 
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset

1315 
4K). Moreover, it is generally more robust than "Nimbus". 
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset

1316 

62163  1317 
* Update to jedit5.3.0, with improved GUI scaling and support of 
1318 
highresolution displays (e.g. 4K). 

1319 

62034  1320 
* The main Isabelle executable is managed as singleinstance Desktop 
1321 
application uniformly on all platforms: Linux, Windows, Mac OS X. 

1322 

60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset

1323 

61405  1324 
*** Document preparation *** 
1325 

62017  1326 
* Commands 'paragraph' and 'subparagraph' provide additional section 
1327 
headings. Thus there are 6 levels of standard headings, as in HTML. 

1328 

1329 
* Command 'text_raw' has been clarified: input text is processed as in 

1330 
'text' (with antiquotations and control symbols). The key difference is 

1331 
the lack of the surrounding isabelle markup environment in output. 

1332 

1333 
* Text is structured in paragraphs and nested lists, using notation that 

1334 
is similar to Markdown. The control symbols for list items are as 

1335 
follows: 

1336 

1337 
\<^item> itemize 

1338 
\<^enum> enumerate 

1339 
\<^descr> description 

1340 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1341 
* There is a new short form for antiquotations with a single argument 
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1342 
that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and 
61595  1343 
\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. 
1344 
\<^name> without following cartouche is equivalent to @{name}. The 

61501  1345 
standard Isabelle fonts provide glyphs to render important control 
1346 
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1347 

61595  1348 
* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with 
1349 
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using 

1350 
standard LaTeX macros of the same names. 

1351 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1352 
* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. 
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1353 
Consequently, \<open>...\<close> without any decoration prints literal quasiformal 
61492  1354 
text. Commandline tool "isabelle update_cartouches t" helps to update 
1355 
old sources, by approximative patching of the content of string and 

1356 
cartouche tokens seen in theory sources. 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1357 

97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1358 
* The @{text} antiquotation now ignores the antiquotation option 
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1359 
"source". The given text content is output unconditionally, without any 
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1360 
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the 
61494  1361 
argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial 
1362 
or terminal spaces are ignored. 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

1363 

62017  1364 
* Antiquotations @{emph} and @{bold} output LaTeX source recursively, 
1365 
adding appropriate text style markup. These may be used in the short 

1366 
form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. 

1367 

1368 
* Document antiquotation @{footnote} outputs LaTeX source recursively, 

1369 
marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. 

1370 

1371 
* Antiquotation @{verbatim [display]} supports option "indent". 

1372 

1373 
* Antiquotation @{theory_text} prints uninterpreted theory source text 

62231
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62209
diff
changeset

1374 
(Isar outer syntax with command keywords etc.). This may be used in the 
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62209
diff
changeset

1375 
short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". 
62017  1376 

1377 
* Antiquotation @{doc ENTRY} provides a reference to the given 

1378 
documentation, with a hyperlink in the Prover IDE. 

1379 

1380 
* Antiquotations @{command}, @{method}, @{attribute} print checked 

1381 
entities of the Isar language. 

1382 

61471  1383 
* HTML presentation uses the standard IsabelleText font and Unicode 
1384 
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former 

61488  1385 
print mode "HTML" loses its special meaning. 
61471  1386 

61405  1387 

60406  1388 
*** Isar *** 
1389 

62205  1390 
* Local goals ('have', 'show', 'hence', 'thus') allow structured rule 
1391 
statements like fixes/assumes/shows in theorem specifications, but the 

1392 
notation is postfix with keywords 'if' (or 'when') and 'for'. For 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

1393 
example: 
60414  1394 

1395 
have result: "C x y" 

1396 
if "A x" and "B y" 

1397 
for x :: 'a and y :: 'a 

1398 
<proof> 

1399 

60449  1400 
The local assumptions are bound to the name "that". The result is 
1401 
exported from context of the statement as usual. The above roughly 

60414  1402 
corresponds to a raw proof block like this: 
1403 

1404 
{ 

1405 
fix x :: 'a and y :: 'a 

60449  1406 
assume that: "A x" "B y" 
60414  1407 
have "C x y" <proof> 
1408 
} 

1409 
note result = this 

60406  1410 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

1411 
The keyword 'when' may be used instead of 'if', to indicate 'presume' 
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

1412 
instead of 'assume' above. 
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

1413 

61733  1414 
* Assumptions ('assume', 'presume') allow structured rule statements 
1415 
using 'if' and 'for', similar to 'have' etc. above. For example: 

61658  1416 

1417 
assume result: "C x y" 

1418 
if "A x" and "B y" 

1419 
for x :: 'a and y :: 'a 

1420 

1421 
This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general 

1422 
result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y". 

1423 

1424 
Vacuous quantification in assumptions is omitted, i.e. a forcontext 

1425 
only effects propositions according to actual use of variables. For 

1426 
example: 

1427 

1428 
assume "A x" and "B y" for x and y 

1429 

1430 
is equivalent to: 

1431 

1432 
assume "\<And>x. A x" and "\<And>y. B y" 

1433 

60595  1434 
* The meaning of 'show' with Pure rule statements has changed: premises 
1435 
are treated in the sense of 'assume', instead of 'presume'. This means, 

62205 </ 