author  haftmann 
Thu, 06 Apr 2017 21:37:13 +0200  
changeset 65417  fc41a5650fb1 
parent 65396  b42167902f57 
child 65448  9bc3b57c1fa7 
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 

64986  10 
*** General *** 
11 

12 
* Document antiquotations @{prf} and @{full_prf} output proof terms 

13 
(again) in the same way as commands 'prf' and 'full_prf'. 

14 

65055  15 
* Computations generated by the code generator can be embedded directly 
16 
into ML, alongside with @{code} antiquotations, using the following 

17 
antiquotations: 

18 

19 
@{computation ... terms: ... datatypes: ...} : 

20 
((term > term) > 'ml option > 'a) > Proof.context > term > 'a 

21 
@{computation_conv ... terms: ... datatypes: ...} : 

22 
(Proof.context > 'ml > conv) > Proof.context > conv 

65045
b69ef432438d
avoid Unicode that conflicts with Isabelle symbol rendering;
wenzelm
parents:
65042
diff
changeset

23 
@{computation_check terms: ... datatypes: ...} : Proof.context > conv 
65041  24 

65055  25 
See src/HOL/ex/Computations.thy, 
26 
src/HOL/Decision_Procs/Commutative_Ring.thy and 

27 
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the 

28 
tutorial on code generation. 

65041  29 

64986  30 

64602  31 
*** Prover IDE  Isabelle/Scala/jEdit *** 
32 

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

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

35 
used for formal checking. 

36 

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

39 
changes of formal document content. Theory dependencies are always 

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

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

42 
effectively always enabled. 

43 

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

46 
buffers. 

47 

65329  48 
* Update to jedit5.4.0. 
49 

64602  50 

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

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

52 

65396
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
65329
diff
changeset

53 
* Constants E/L/F in Library/Formal_Power_Series were renamed to 
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
65329
diff
changeset

54 
fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space. 
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
65329
diff
changeset

55 
INCOMPATIBILITY. 
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
65329
diff
changeset

56 

65417  57 
* Session "Computional_Algebra" covers many previously scattered 
58 
theories, notably Euclidean_Algorithm, Factorial_Ring, Formal_Power_Series, 

59 
Fraction_Field, Fundamental_Theorem_Algebra, Normalized_Fraction, 

60 
Polynomial_FPS, Polynomial, Primes. Minor INCOMPATIBILITY. 

61 

65170
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset

62 
* Constant "surj" is a full input/output abbreviation (again). 
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset

63 
Minor INCOMPATIBILITY. 
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset

64 

65050  65 
* Theory Library/FinFun has been moved to AFP (again). INCOMPATIBILITY. 
66 

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

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

70 
simplify porting old theories: 

71 

72 
syntax (ASCII) 

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

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

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

76 

64632  77 
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively. 
78 
INCOMPATIBILITY. 

79 

65064
a4abec71279a
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
paulson <lp15@cam.ac.uk>
parents:
65057
diff
changeset

80 
* Renamed ii to imaginary_unit in order to free up ii as a variable name. 
a4abec71279a
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
paulson <lp15@cam.ac.uk>
parents:
65057
diff
changeset

81 
The syntax \<i> remains available. 
a4abec71279a
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
paulson <lp15@cam.ac.uk>
parents:
65057
diff
changeset

82 
INCOMPATIBILITY. 
a4abec71279a
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
paulson <lp15@cam.ac.uk>
parents:
65057
diff
changeset

83 

64787  84 
* Dropped abbreviations transP, antisymP, single_valuedP; 
64634  85 
use constants transp, antisymp, single_valuedp instead. 
86 
INCOMPATIBILITY. 

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

87 

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

90 
unique_euclidean_(semi)ring; instantiation requires 

91 
provision of a euclidean size. 

92 

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

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

94 
 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

95 
 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

96 
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

97 
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

98 
 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

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

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

101 

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

104 
INCOMPATIBILITY. 

105 

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

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

107 
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

108 
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

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

110 

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

111 
* Generalized some facts: 
64876  112 
measure_induct_rule 
113 
measure_induct 

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

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

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

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

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

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

119 

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

120 
* (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

121 
 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

122 
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

123 
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

124 

65099
30d0b2f1df76
KnasterTarski fixed point theorem and Galois Connections.
ballarin
parents:
65073
diff
changeset

125 
* Session HOLAlgebra extended by additional lattice theory: the 
30d0b2f1df76
KnasterTarski fixed point theorem and Galois Connections.
ballarin
parents:
65073
diff
changeset

126 
KnasterTarski fixed point theorem and Galois Connections. 
30d0b2f1df76
KnasterTarski fixed point theorem and Galois Connections.
ballarin
parents:
65073
diff
changeset

127 

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

65057
799bbbb3a395
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents:
65056
diff
changeset

130 
Curve Theorem and the Great Picard Theorem. 
64846  131 

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

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

133 
bij_swap_ompose_bij ~> bij_swap_compose_bij 
64602  134 

65055  135 
* Session HOLLibrary: The simprocs on subsets operators of multisets 
136 
have been renamed: 

65027
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64986
diff
changeset

137 
msetless_cancel_numerals ~> msetsubset_cancel 
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64986
diff
changeset

138 
msetle_cancel_numerals ~> msetsubset_eq_cancel 
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64986
diff
changeset

139 
INCOMPATIBILITY. 
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64986
diff
changeset

140 

65055  141 
* Session HOLLibrary: The suffix _numerals has been removed from the 
142 
name of the simprocs on multisets. INCOMPATIBILITY. 

65027
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64986
diff
changeset

143 

60331  144 

64844  145 
*** System *** 
146 

65056  147 
* Option parallel_proofs is 1 by default (instead of more aggressive 2). 
148 
This requires less heap space and avoids burning parallel CPU cycles, 

149 
while full subproof parallelization is enabled for repeated builds 

150 
(according to parallel_subproofs_threshold). 

151 

64844  152 
* Prover IDE support for the Visual Studio Code editor and language 
153 
server protocol, via the "isabelle vscode_server" tool (see also 

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

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

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

157 
frontends. 

158 

64900  159 
* ISABELLE_SCALA_BUILD_OPTIONS has been renamed to 
160 
ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY. 

161 

65073  162 
* Isabelle settings ISABELLE_WINDOWS_PLATFORM, 
163 
ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the 

164 
native Windows platform (independently of the Cygwin installation). This 

165 
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32, 

166 
ISABELLE_PLATFORM64. 

65072  167 

64900  168 

64844  169 

64072  170 
New in Isabelle20161 (December 2016) 
171 
 

62216  172 

62440  173 
*** General *** 
174 

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

177 
INCOMPATIBILITY. 

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

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

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

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

182 
result the subgoal may be split into several subgoals. 

183 

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

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

187 

188 
bundle foo 

189 
begin 

190 
declare a [simp] 

191 
declare b [intro] 

192 
end 

63272  193 

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

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

197 

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

200 
discontinued. 

201 

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

203 
delimited uniformly via cartouches. This works better than oldfashioned 

204 
quotes when sublanguages are nested. 

205 

206 
* Mixfix annotations support general block properties, with syntax 

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

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

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

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

63650  211 

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

214 

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

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

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

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

220 
examples. 

221 

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

223 
instances) are generated into companion object of corresponding type 

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

225 

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

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

228 

64602  229 

62904  230 
*** Prover IDE  Isabelle/Scala/jEdit *** 
231 

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

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

235 
reactivity and CPU usage. 

236 

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

239 
command keywords and some command substructure. Action 

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

241 
according to command keywords only; see also option 

242 
"jedit_indent_newline". 

243 

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

245 
number of subgoals. This requires information of ongoing document 

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

247 
quickly; see also option "jedit_script_indent" and 

248 
"jedit_script_indent_limit". 

249 

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

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

252 
structure of theory specifications is treated as well. 

253 

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

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

256 

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

258 
e.g. 'context', 'notepad'. 

259 

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

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

262 

63977  263 
* Highlighting of entity def/ref positions wrt. cursor. 
264 

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

64514  266 
occurrences of the formal entity at the caret position. This facilitates 
63977  267 
systematic renaming. 
268 

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

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

271 
theorem statement. 

272 

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

274 
situations where old ASCII notation may be updated. 

275 

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

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

279 
inaccessible via keyboard completion). 

280 

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

283 

284 
src/Pure/ROOT0.ML 

285 
src/Pure/ROOT.ML 

286 
src/Pure/Pure.thy 

287 
src/Pure/ML_Bootstrap.thy 

288 

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

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

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

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

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

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

63307  295 
dependencies of the above files are only observed for batch build. 
62904  296 

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

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

63461  300 

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

304 
new 'abbrevs' section. 

305 

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

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

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

63579  309 

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

312 
keymap; nonconflicting changes are always applied implicitly. This 

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

314 
increases chances that users see new keyboard shortcuts when reusing 

315 
old keymaps. 

316 

63675  317 
* ML and document antiquotations for filesystems paths are more uniform 
318 
and diverse: 

319 

320 
@{path NAME}  no filesystem check 

321 
@{file NAME}  check for plain file 

322 
@{dir NAME}  check for directory 

323 

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

325 
have to be changed. 

63669  326 

327 

63977  328 
*** Document preparation *** 
329 

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

331 

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

334 

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

337 

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

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

340 
derivatives. 

341 

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

343 

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

345 
Isabelle2015). 

346 

347 

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

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

349 

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

352 
'definition', 'inductive', 'function'. 

353 

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

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

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

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

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

359 

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

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

63039  364 

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

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

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

367 

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

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

369 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  370 

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

373 

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

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

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

377 

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

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

380 
INCOMPATIBILITY. 

62939  381 

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

384 
definitions. 

385 

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

63259  388 

389 
(use facts in simp) 

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

391 

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

394 

62216  395 

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

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

397 

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

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

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

402 

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

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

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

406 
regardless of the actual parameters that are provided. Rare 

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

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

409 

410 
* Typeinference improves sorts of newly introduced type variables for 

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

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

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

414 
INCOMPATIBILITY, need to provide explicit type constraints for Pure 

415 
types where this is really intended. 

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

416 

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

417 

62327  418 
*** HOL *** 
419 

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

422 
propositional logic, goals based on a combination of quantifierfree 

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

424 
quantifierfree propositional logic with linear real arithmetic 

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

426 

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

429 

63977  430 
* Metis: The problem encoding has changed very slightly. This might 
63785  431 
break existing proofs. INCOMPATIBILITY. 
432 

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

434 
 The MaSh relevance filter is now faster than before. 
63116  435 
 Produce syntactically correct Vampire 4.0 problem files. 
436 

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

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

62842  441 
method. See 'isabelle doc corec'. 
63977  442 
 The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a firstclass 
63855  443 
citizen in bounded natural functors. 
62693  444 
 'primrec' now allows nested calls through the predicator in addition 
62327  445 
to the map function. 
63855  446 
 'bnf' automatically discharges reflexive proof obligations. 
62693  447 
 'bnf' outputs a slightly modified proof obligation expressing rel in 
62332  448 
terms of map and set 
63855  449 
(not giving a specification for rel makes this one reflexive). 
62693  450 
 'bnf' outputs a new proof obligation expressing pred in terms of set 
63855  451 
(not giving a specification for pred makes this one reflexive). 
452 
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. 

62335  453 
 Renamed lemmas: 
454 
rel_prod_apply ~> rel_prod_inject 

455 
pred_prod_apply ~> pred_prod_inject 

456 
INCOMPATIBILITY. 

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

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

460 
INCOMPATIBILITY. 

62327  461 

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

464 
which exposed details of the internal fixpoint construction and was 

465 
hard to use. INCOMPATIBILITY. 

466 

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

468 

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

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

471 

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

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

474 
eliminated altogether. 

475 

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

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

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

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

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

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

482 
INCOMPATIBILITY in rare situations. 

483 

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

485 
INCOMPATIBILITY. 

486 

64390  487 
* Renamed constants and corresponding theorems: 
488 

489 
setsum ~> sum 

490 
setprod ~> prod 

491 
listsum ~> sum_list 

492 
listprod ~> prod_list 

493 

494 
INCOMPATIBILITY. 

495 

496 
* Sligthly more standardized theorem names: 

497 
sgn_times ~> sgn_mult 

498 
sgn_mult' ~> Real_Vector_Spaces.sgn_mult 

499 
divide_zero_left ~> div_0 

500 
zero_mod_left ~> mod_0 

501 
divide_zero ~> div_by_0 

502 
divide_1 ~> div_by_1 

503 
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left 

504 
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left 

505 
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right 

506 
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right 

507 
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left 

508 
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right 

509 
mod_div_equality ~> div_mult_mod_eq 

510 
mod_div_equality2 ~> mult_div_mod_eq 

511 
mod_div_equality3 ~> mod_div_mult_eq 

512 
mod_div_equality4 ~> mod_mult_div_eq 

513 
minus_div_eq_mod ~> minus_div_mult_eq_mod 

514 
minus_div_eq_mod2 ~> minus_mult_div_eq_mod 

515 
minus_mod_eq_div ~> minus_mod_eq_div_mult 

516 
minus_mod_eq_div2 ~> minus_mod_eq_mult_div 

517 
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] 

518 
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] 

519 
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] 

520 
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] 

521 
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

522 
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

523 
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

524 
div_1 ~> div_by_Suc_0 

525 
mod_1 ~> mod_by_Suc_0 

526 
INCOMPATIBILITY. 

527 

528 
* New type class "idom_abs_sgn" specifies algebraic properties 

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

530 
disappeared. Slight INCOMPATIBILITY. 

531 

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

533 

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

536 

537 
 Logical representation: 

538 
* 0 is instantiated to the ASCII zero character. 

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

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

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

542 
are noncanonical. 

543 
 Printing and parsing: 

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

545 
(as before). 

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

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

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

549 
is parsable for every numeral expression n. 

550 
* Noncanonical characters have no special syntax and are 

551 
printed as their logical representation. 

552 
 Explicit conversions from and to the natural numbers are 

553 
provided as char_of_nat, nat_of_char (as before). 

554 
 The auxiliary nibble type has been discontinued. 

555 

556 
INCOMPATIBILITY. 

557 

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

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

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

561 
infix "mod" syntax. INCOMPATIBILITY. 

562 

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

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

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

567 
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY. 

568 

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

571 

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

573 
which renders those abstract effectively. 

574 

575 
* Command 'export_code' checks given constants for abstraction 

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

577 
interface for the generated code. 

578 

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

580 
spelt out explicitly. 

581 

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

583 
explicitly provided auxiliary definitions for required type class 

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

586 

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

588 
products. 

63977  589 

590 
* Locale bijection establishes convenient default simp rules such as 

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

592 

593 
* Abstract locales semigroup, abel_semigroup, semilattice, 

594 
semilattice_neutr, ordering, ordering_top, semilattice_order, 

595 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 

596 
semilattice_neutr_set, semilattice_order_set, 

597 
semilattice_order_neutr_set monoid_list, comm_monoid_list, 

598 
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified 

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

600 
INCOMPATIBILITY. 

601 

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

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

604 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

605 

63807  606 
* Some old / obsolete theorems have been renamed / removed, potential 
607 
INCOMPATIBILITY. 

608 

609 
nat_less_cases  removed, use linorder_cases instead 

610 
inv_image_comp  removed, use image_inv_f_f instead 

611 
image_surj_f_inv_f ~> image_f_inv_f 

63113  612 

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

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

614 
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

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

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

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

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

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

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

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

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

623 

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

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

625 
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

626 
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

627 
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

628 
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

629 
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

630 
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

631 
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

632 
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

633 
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

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

635 

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

62396  638 

63977  639 
* Added class topological_monoid. 
640 

64391  641 
* The following theorems have been renamed: 
642 

64457  643 
setsum_left_distrib ~> sum_distrib_right 
644 
setsum_right_distrib ~> sum_distrib_left 

64391  645 

646 
INCOMPATIBILITY. 

647 

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

649 
INCOMPATIBILITY. 

650 

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

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

653 
A)". 

654 

655 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 

656 

657 
* The type class ordered_comm_monoid_add is now called 

658 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 

659 
is introduced as the combination of ordered_ab_semigroup_add + 

660 
comm_monoid_add. INCOMPATIBILITY. 

661 

662 
* Introduced the type classes canonically_ordered_comm_monoid_add and 

663 
dioid. 

664 

665 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 

666 
instantiating linordered_semiring_strict and ordered_ab_group_add, an 

667 
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 

668 
be required. INCOMPATIBILITY. 

63117  669 

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

672 
lcm_left_commute_nat ~> lcm.left_commute 

673 
lcm_left_commute_int ~> lcm.left_commute 

674 
gcd_left_commute_nat ~> gcd.left_commute 

675 
gcd_left_commute_int ~> gcd.left_commute 

676 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

677 
gcd_greatest_iff_int ~> gcd_greatest_iff 

678 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

679 
coprime_dvd_mult_int ~> coprime_dvd_mult 

680 
zpower_numeral_even ~> power_numeral_even 

681 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

682 
gcd_mult_cancel_int ~> gcd_mult_cancel 

683 
div_gcd_coprime_nat ~> div_gcd_coprime 

684 
div_gcd_coprime_int ~> div_gcd_coprime 

685 
zpower_numeral_odd ~> power_numeral_odd 

686 
zero_less_int_conv ~> of_nat_0_less_iff 

687 
gcd_greatest_nat ~> gcd_greatest 

688 
gcd_greatest_int ~> gcd_greatest 

689 
coprime_mult_nat ~> coprime_mult 

690 
coprime_mult_int ~> coprime_mult 

691 
lcm_commute_nat ~> lcm.commute 

692 
lcm_commute_int ~> lcm.commute 

693 
int_less_0_conv ~> of_nat_less_0_iff 

694 
gcd_commute_nat ~> gcd.commute 

695 
gcd_commute_int ~> gcd.commute 

696 
Gcd_insert_nat ~> Gcd_insert 

697 
Gcd_insert_int ~> Gcd_insert 

698 
of_int_int_eq ~> of_int_of_nat_eq 

699 
lcm_least_nat ~> lcm_least 

700 
lcm_least_int ~> lcm_least 

701 
lcm_assoc_nat ~> lcm.assoc 

702 
lcm_assoc_int ~> lcm.assoc 

703 
int_le_0_conv ~> of_nat_le_0_iff 

704 
int_eq_0_conv ~> of_nat_eq_0_iff 

705 
Gcd_empty_nat ~> Gcd_empty 

706 
Gcd_empty_int ~> Gcd_empty 

707 
gcd_assoc_nat ~> gcd.assoc 

708 
gcd_assoc_int ~> gcd.assoc 

709 
zero_zle_int ~> of_nat_0_le_iff 

710 
lcm_dvd2_nat ~> dvd_lcm2 

711 
lcm_dvd2_int ~> dvd_lcm2 

712 
lcm_dvd1_nat ~> dvd_lcm1 

713 
lcm_dvd1_int ~> dvd_lcm1 

714 
gcd_zero_nat ~> gcd_eq_0_iff 

715 
gcd_zero_int ~> gcd_eq_0_iff 

716 
gcd_dvd2_nat ~> gcd_dvd2 

717 
gcd_dvd2_int ~> gcd_dvd2 

718 
gcd_dvd1_nat ~> gcd_dvd1 

719 
gcd_dvd1_int ~> gcd_dvd1 

720 
int_numeral ~> of_nat_numeral 

721 
lcm_ac_nat ~> ac_simps 

722 
lcm_ac_int ~> ac_simps 

723 
gcd_ac_nat ~> ac_simps 

724 
gcd_ac_int ~> ac_simps 

725 
abs_int_eq ~> abs_of_nat 

726 
zless_int ~> of_nat_less_iff 

727 
zdiff_int ~> of_nat_diff 

728 
zadd_int ~> of_nat_add 

729 
int_mult ~> of_nat_mult 

730 
int_Suc ~> of_nat_Suc 

731 
inj_int ~> inj_of_nat 

732 
int_1 ~> of_nat_1 

733 
int_0 ~> of_nat_0 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

756 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  757 
realpow_minus_mult ~> power_minus_mult 
758 
realpow_Suc_le_self ~> power_Suc_le_self 

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

759 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  760 
INCOMPATIBILITY. 
761 

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

762 
* Renamed HOL/Quotient_Examples/FSet.thy to 
63977  763 
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. 
764 

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

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

768 
"unbundle finfun_syntax" to imitate import of 

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

770 

771 
* Session HOLLibrary: theory Multiset_Permutations (executably) defines 

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

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

774 
once. 

775 

776 
* Session HOLLibrary: multiset membership is now expressed using 

777 
set_mset rather than count. 

778 

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

780 
by default. 

781 

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

783 
equations count_eq_zero_iff and not_in_iff. 

784 

785 
 Rules count_inI and in_countE obtain facts of the form 

786 
"count M a = n" from membership. 

787 

788 
 Rules count_in_diffI and in_diff_countE obtain facts of the form 

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

790 

791 
INCOMPATIBILITY. 

792 

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

794 
displaying equations in functional programming style  variables 

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

796 
underscores. 

797 

798 
* Session HOLLibrary: theory Combinator_PER provides combinator to 

799 
build partial equivalence relations from a predicate and an equivalence 

800 
relation. 

801 

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

803 
everywhere fix bijections. 

804 

805 
* Session HOLLibrary: theory Normalized_Fraction allows viewing an 

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

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

808 
denominator is normalized wrt. unit factors). 

809 

810 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 

811 

812 
* Session HOLMultivariate_Analysis has been renamed to HOLAnalysis. 

813 

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

815 
HOLProbability. When importing HOLAnalysis some theorems need 

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

817 

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

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

820 
principle, Residue theorem, Schwarz Lemma. 

821 

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

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

824 

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

826 
libraries: homeomorphisms, continuous function extensions, invariance of 

827 
domain. 

828 

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

830 
changed from ereal to ennreal, INCOMPATIBILITY. 

831 

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

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

834 

835 
* Session HOLProbability: Code generation and QuickCheck for 

836 
Probability Mass Functions. 

837 

838 
* Session HOLProbability: theory Random_Permutations contains some 

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

840 
folding over a list in random order. 

841 

842 
* Session HOLProbability: theory SPMF formalises discrete 

843 
subprobability distributions. 

844 

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

846 
normalised to distinguish which ordering the theorems are about 

847 

848 
mset_less_eqI ~> mset_subset_eqI 

849 
mset_less_insertD ~> mset_subset_insertD 

850 
mset_less_eq_count ~> mset_subset_eq_count 

851 
mset_less_diff_self ~> mset_subset_diff_self 

852 
mset_le_exists_conv ~> mset_subset_eq_exists_conv 

853 
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel 

854 
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel 

855 
mset_le_mono_add ~> mset_subset_eq_mono_add 

856 
mset_le_add_left ~> mset_subset_eq_add_left 

857 
mset_le_add_right ~> mset_subset_eq_add_right 

858 
mset_le_single ~> mset_subset_eq_single 

859 
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute 

860 
diff_le_self ~> diff_subset_eq_self 

861 
mset_leD ~> mset_subset_eqD 

862 
mset_lessD ~> mset_subsetD 

863 
mset_le_insertD ~> mset_subset_eq_insertD 

864 
mset_less_of_empty ~> mset_subset_of_empty 

865 
mset_less_size ~> mset_subset_size 

866 
wf_less_mset_rel ~> wf_subset_mset_rel 

867 
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq 

868 
mset_remdups_le ~> mset_remdups_subset_eq 

869 
ms_lesseq_impl ~> subset_eq_mset_impl 

870 

871 
Some functions have been renamed: 

872 
ms_lesseq_impl > subset_eq_mset_impl 

873 

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

875 
#\<subseteq># ~> \<le> 

876 
#\<subset># ~> < 

877 
le_multiset ~> less_eq_multiset 

878 
less_multiset ~> le_multiset 

879 
INCOMPATIBILITY. 

880 

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

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

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

884 
interpretations "multiset_linorder" and "multiset_wellorder" have been 

885 
replaced by instantiations. INCOMPATIBILITY. 

886 

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

888 
been renamed: 

889 

890 
le_multiset_def ~> less_eq_multiset_def 

891 
less_multiset_def ~> le_multiset_def 

892 
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset 

893 
mult_less_not_refl ~> mset_le_not_refl 

894 
mult_less_trans ~> mset_le_trans 

895 
mult_less_not_sym ~> mset_le_not_sym 

896 
mult_less_asym ~> mset_le_asym 

897 
mult_less_irrefl ~> mset_le_irrefl 

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

899 

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

901 
le_multiset_total ~> less_eq_multiset_total 

902 
less_multiset_right_total ~> subset_eq_imp_le_multiset 

903 
le_multiset_empty_left ~> less_eq_multiset_empty_left 

904 
le_multiset_empty_right ~> less_eq_multiset_empty_right 

905 
less_multiset_empty_right ~> le_multiset_empty_left 

906 
less_multiset_empty_left ~> le_multiset_empty_right 

907 
union_less_diff_plus ~> union_le_diff_plus 

908 
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset 

909 
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty 

910 
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty 

911 
INCOMPATIBILITY. 

912 

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

914 
INCOMPATIBILITY. 

915 

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

917 
INCOMPATIBILITY, use the following replacements: 

918 

919 
le_multiset_plus_plus_left_iff ~> add_less_cancel_right 

920 
less_multiset_plus_plus_left_iff ~> add_less_cancel_right 

921 
le_multiset_plus_plus_right_iff ~> add_less_cancel_left 

922 
less_multiset_plus_plus_right_iff ~> add_less_cancel_left 

923 
add_eq_self_empty_iff ~> add_cancel_left_right 

924 
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right 

925 
mset_less_add_bothsides ~> subset_mset.add_less_cancel_right 

926 
mset_le_add_bothsides ~> subset_mset.add_less_cancel_right 

927 
empty_inter ~> subset_mset.inf_bot_left 

928 
inter_empty ~> subset_mset.inf_bot_right 

929 
empty_sup ~> subset_mset.sup_bot_left 

930 
sup_empty ~> subset_mset.sup_bot_right 

931 
bdd_below_multiset ~> subset_mset.bdd_above_bot 

932 
subset_eq_empty ~> subset_mset.le_zero_eq 

933 
le_empty ~> subset_mset.le_zero_eq 

934 
mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

935 
mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

936 

937 
* Session HOLLibrary: some typeclass constraints about multisets have 

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

939 
additional typeclasses order_bot, no_top, 

940 
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, 

941 
linordered_cancel_ab_semigroup_add, and 

942 
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. 

943 

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

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

946 
INCOMPATIBILITY. 

947 

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

949 
interpretations ordered_ab_semigroup_monoid_add_imp_le and 

950 
bounded_lattice_bot. INCOMPATIBILITY. 

951 

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

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

954 
removed or changed: 

955 

956 
single_not_empty ~> add_mset_not_empty or empty_not_add_mset 

957 
fold_mset_insert ~> fold_mset_add_mset 

958 
image_mset_insert ~> image_mset_add_mset 

959 
union_single_eq_diff 

960 
multi_self_add_other_not_self 

961 
diff_single_eq_union 

962 
INCOMPATIBILITY. 

963 

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

965 
to use add_mset instead of single: 

966 

967 
mset_add 

968 
multi_self_add_other_not_self 

969 
diff_single_eq_union 

970 
union_single_eq_diff 

971 
union_single_eq_member 

972 
add_eq_conv_diff 

973 
insert_noteq_member 

974 
add_eq_conv_ex 

975 
multi_member_split 

976 
multiset_add_sub_el_shuffle 

977 
mset_subset_eq_insertD 

978 
mset_subset_insertD 

979 
insert_subset_eq_iff 

980 
insert_union_subset_iff 

981 
multi_psub_of_add_self 

982 
inter_add_left1 

983 
inter_add_left2 

984 
inter_add_right1 

985 
inter_add_right2 

986 
sup_union_left1 

987 
sup_union_left2 

988 
sup_union_right1 

989 
sup_union_right2 

990 
size_eq_Suc_imp_eq_union 

991 
multi_nonempty_split 

992 
mset_insort 

993 
mset_update 

994 
mult1I 

995 
less_add 

996 
mset_zip_take_Cons_drop_twice 

997 
rel_mset_Zero 

998 
msed_map_invL 

999 
msed_map_invR 

1000 
msed_rel_invL 

1001 
msed_rel_invR 

1002 
le_multiset_right_total 

1003 
multiset_induct 

1004 
multiset_induct2_size 

1005 
multiset_induct2 

1006 
INCOMPATIBILITY. 

1007 

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

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

1010 
element: 

1011 

1012 
image_mset 

1013 
mset 

1014 
replicate_mset 

1015 
mult1 

1016 
pred_mset 

1017 
rel_mset' 

1018 
mset_insort 

1019 

1020 
INCOMPATIBILITY. 

1021 

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

1023 
attributes of some multiset theorems have been changed: 

1024 

1025 
insert_DiffM [] ~> [simp] 

1026 
insert_DiffM2 [simp] ~> [] 

1027 
diff_add_mset_swap [simp] 

1028 
fold_mset_add_mset [simp] 

1029 
diff_diff_add [simp] (for multisets only) 

1030 
diff_cancel [simp] ~> [] 

1031 
count_single [simp] ~> [] 

1032 
set_mset_single [simp] ~> [] 

1033 
size_multiset_single [simp] ~> [] 

1034 
size_single [simp] ~> [] 

1035 
image_mset_single [simp] ~> [] 

1036 
mset_subset_eq_mono_add_right_cancel [simp] ~> [] 

1037 
mset_subset_eq_mono_add_left_cancel [simp] ~> [] 

1038 
fold_mset_single [simp] ~> [] 

1039 
subset_eq_empty [simp] ~> [] 

1040 
empty_sup [simp] ~> [] 

1041 
sup_empty [simp] ~> [] 

1042 
inter_empty [simp] ~> [] 

1043 
empty_inter [simp] ~> [] 

1044 
INCOMPATIBILITY. 

1045 

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

1049 
INCOMPATIBILITY. 

1050 

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

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

1053 
natural numbers. INCOMPATIBILITY. 

1054 

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

1056 
multisets: 

1057 

1058 
msetsum ~> sum_mset 

1059 
msetprod ~> prod_mset 

1060 

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

1062 
and union of multisets have been changed: 

1063 

1064 
#\<inter> ~> \<inter># 

1065 
#\<union> ~> \<union># 

1066 

1067 
INCOMPATIBILITY. 

1068 

1069 
* Session HOLLibrary, theory Multiset: the lemma 

1070 
one_step_implies_mult_aux on multisets has been removed, use 

1071 
one_step_implies_mult instead. INCOMPATIBILITY. 

1072 

1073 
* Session HOLLibrary: theory Complete_Partial_Order2 provides reasoning 

1074 
support for monotonicity and continuity in chaincomplete partial orders 

1075 
and about admissibility conditions for fixpoint inductions. 

1076 

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

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

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

1081 
future different type class instantiation for polynomials over factorial 

1082 
rings. INCOMPATIBILITY. 

64390  1083 

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

1085 
the following renaming 

1086 

1087 
prefixeq > prefix 

1088 
prefix > strict_prefix 

1089 
suffixeq > suffix 

1090 
suffix > strict_suffix 

1091 

1092 
Added theory of longest common prefixes. 

64389  1093 

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

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

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

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

1099 
"prime_nat_iff". INCOMPATIBILITY. 

1100 

1101 
* Session Old_Number_Theory has been removed, after porting remaining 

1102 
theories. 

1103 

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

1106 

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

1107 

62498  1108 
*** ML *** 
1109 

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

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

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

1114 
INCOMPATIBILITY. 

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

1115 

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

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

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

1123 

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

1126 

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

1128 
with approximative output quality. 

1129 

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

1131 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 

1132 

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

1135 
requiring separate files. 

1136 

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

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

1140 
debugger information requires consirable time and space: main 

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

1142 

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

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

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

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

1148 
balanced blocks of Local_Theory.open_target versus 

1149 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

1150 

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

1153 
INCOMPATIBILITY. 

1154 

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

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

1158 
File.full_path). Potential INCOMPATIBILITY. 

1159 

63352  1160 
* Binding.empty_atts supersedes Thm.empty_binding and 
1161 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

1162 

62498  1163 

62354  1164 
*** System *** 
1165 

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

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

1169 
much less disk space. 

63226  1170 

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

1173 
particular: 

1174 

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

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

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

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

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

1179 

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

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

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

1183 

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

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

1185 
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

1186 
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

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

1188 

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

1191 
servers with separate CPU/memory modules. 

1192 

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

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

64274  1195 
unless there is already a default provided via ML_OPTIONS settings. 
1196 

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

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

1198 
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

1199 
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

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

1201 

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

1205 
resulting log files. 

64308  1206 

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

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

1208 
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

1209 
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

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

1211 

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

1214 

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

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

1217 
Isabelle/ML or Isabelle/Scala. 

1218 

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

1220 
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, 

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

1222 
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been 

1223 
discontinued. Potential INCOMPATIBILITY. 

1224 

1225 
* The Isabelle system environment always ensures that the main 

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

1227 
"isabelle_scala_script". 

1228 

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

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

1231 
Isabelle_Tool.Body. 

1232 

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

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

1235 
produce robust shell scripts under program control, without worrying 

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

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

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

1239 
been discontinued. 

1240 

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

1243 
but without the Isabelle settings environment. 

1244 

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

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

1248 
that Path specifications need to be resolved remotely via 

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

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

1251 

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

1253 
regular hg commandline interface. The repositroy clone and working 

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

1255 
connection). 

64265  1256 

62354  1257 

1258 

62031  1259 
New in Isabelle2016 (February 2016) 
62016  1260 
 
60138  1261 

61337  1262 
*** General *** 
1263 

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

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

1265 
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

1266 
~~/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

1267 
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

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

1269 

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

1272 

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

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

1276 
has been removed (see below). 

1277 

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

62017  1280 

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

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

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

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

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

1285 

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

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

1287 
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

1288 
\<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

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

1290 

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

1293 
to update old sources. 

1294 

61337  1295 
* Toplevel theorem statements have been simplified as follows: 
1296 

1297 
theorems ~> lemmas 

1298 
schematic_lemma ~> schematic_goal 

1299 
schematic_theorem ~> schematic_goal 

1300 
schematic_corollary ~> schematic_goal 

1301 

1302 
Commandline tool "isabelle update_theorems" updates theory sources 

1303 
accordingly. 

1304 

61338  1305 
* Toplevel theorem statement 'proposition' is another alias for 
1306 
'theorem'. 

1307 

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

1310 
deferred definitions require a surrounding 'overloading' block. 

1311 

61337  1312 

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

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

1314 

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

1318 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

1322 
any effect on the running ML program. 

60984  1323 

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

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

1327 
update. 

61729  1328 

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

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

1331 
enable option "editor_output_state". 

61215  1332 

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

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

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

1337 
visibility. 

1338 

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

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

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

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

1343 
panel. 

1344 

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

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

1346 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1347 

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

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

1350 
implicit: a popup will show up unconditionally. 

1351 

1352 
* Additional abbreviations for syntactic completion may be specified in 

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

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

1355 

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

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

1357 
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

1358 
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

1359 
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

1360 

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

1363 
the editor. 

1364 

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

1366 
instead of former C+e LEFT. 

1367 

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

1368 
* The commandline tool "isabelle jedit" and the isabelle.Main 
62027  1369 
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

1370 
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

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

1372 

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

1375 
singleinstance applications seen on common GUI desktops. 

1376 

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

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

1378 
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

1379 
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

1380 

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

1383 

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

1386 

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

1387 

61405  1388 
*** Document preparation *** 
1389 

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

1392 

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

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

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

1396 

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

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

1399 
follows: 

1400 

1401 
\<^item> itemize 

1402 
\<^enum> enumerate 

1403 
\<^descr> description 

1404 

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

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

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

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

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

1411 

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

1414 
standard LaTeX macros of the same names. 

1415 

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

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

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

1420 
cartouche tokens seen in theory sources. 

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

1421 

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

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

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

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

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

1427 

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

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

1431 
