author  haftmann 
Wed, 22 Feb 2017 20:24:50 +0100  
changeset 65041  2525e680f94f 
parent 65027  2b8583507891 
child 65042  956ea00a162a 
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 

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

17 
the following antiquotations: 

18 

19 
@{computation … terms: … datatypes: …} : ((term > term) > 'ml option > 'a) > Proof.context > term > 'a 

20 
@{computation_conv … terms: … datatypes: …} : ('ml > conv) > Proof.context > conv 

21 
@{computation_check terms: … datatypes: …} : Proof.context > conv 

22 

23 
See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy 

24 
and src/HOL/Decision_Procs/Reflective_Field.thy for examples. 

25 

64986  26 

64602  27 
*** Prover IDE  Isabelle/Scala/jEdit *** 
28 

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

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

31 
used for formal checking. 

32 

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

35 
changes of formal document content. Theory dependencies are always 

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

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

38 
effectively always enabled. 

39 

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

42 
buffers. 

43 

64602  44 

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

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

46 

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

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

50 
simplify porting old theories: 

51 

52 
syntax (ASCII) 

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

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

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

56 

64632  57 
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively. 
58 
INCOMPATIBILITY. 

59 

64787  60 
* Dropped abbreviations transP, antisymP, single_valuedP; 
64634  61 
use constants transp, antisymp, single_valuedp instead. 
62 
INCOMPATIBILITY. 

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

63 

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

66 
unique_euclidean_(semi)ring; instantiation requires 

67 
provision of a euclidean size. 

68 

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

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

70 
 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

71 
 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

72 
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

73 
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

74 
 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

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

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

77 

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

80 
INCOMPATIBILITY. 

81 

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

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

83 
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

84 
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

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

86 

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

87 
* Generalized some facts: 
64876  88 
measure_induct_rule 
89 
measure_induct 

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

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

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

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

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

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

95 

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

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

97 
 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

98 
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

99 
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

100 

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

103 
Curve Theorem. 

64846  104 

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

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

106 
bij_swap_ompose_bij ~> bij_swap_compose_bij 
64602  107 

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

108 
* Session HOLLibrary: The simprocs on subsets operators of multisets have been renamed: 
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64986
diff
changeset

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

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

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

112 

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

113 
* Session HOLLibrary: The suffix _numerals has been removed from the name of the simprocs on multisets. 
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64986
diff
changeset

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

115 

60331  116 

64844  117 
*** System *** 
118 

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

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

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

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

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

124 
frontends. 

125 

64900  126 
* ISABELLE_SCALA_BUILD_OPTIONS has been renamed to 
127 
ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY. 

128 

129 

64844  130 

64072  131 
New in Isabelle20161 (December 2016) 
132 
 

62216  133 

62440  134 
*** General *** 
135 

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

138 
INCOMPATIBILITY. 

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

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

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

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

143 
result the subgoal may be split into several subgoals. 

144 

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

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

148 

149 
bundle foo 

150 
begin 

151 
declare a [simp] 

152 
declare b [intro] 

153 
end 

63272  154 

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

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

158 

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

161 
discontinued. 

162 

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

164 
delimited uniformly via cartouches. This works better than oldfashioned 

165 
quotes when sublanguages are nested. 

166 

167 
* Mixfix annotations support general block properties, with syntax 

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

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

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

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

63650  172 

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

175 

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

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

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

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

181 
examples. 

182 

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

184 
instances) are generated into companion object of corresponding type 

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

186 

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

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

189 

64602  190 

62904  191 
*** Prover IDE  Isabelle/Scala/jEdit *** 
192 

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

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

196 
reactivity and CPU usage. 

197 

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

200 
command keywords and some command substructure. Action 

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

202 
according to command keywords only; see also option 

203 
"jedit_indent_newline". 

204 

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

206 
number of subgoals. This requires information of ongoing document 

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

208 
quickly; see also option "jedit_script_indent" and 

209 
"jedit_script_indent_limit". 

210 

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

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

213 
structure of theory specifications is treated as well. 

214 

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

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

217 

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

219 
e.g. 'context', 'notepad'. 

220 

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

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

223 

63977  224 
* Highlighting of entity def/ref positions wrt. cursor. 
225 

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

64514  227 
occurrences of the formal entity at the caret position. This facilitates 
63977  228 
systematic renaming. 
229 

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

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

232 
theorem statement. 

233 

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

235 
situations where old ASCII notation may be updated. 

236 

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

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

240 
inaccessible via keyboard completion). 

241 

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

244 

245 
src/Pure/ROOT0.ML 

246 
src/Pure/ROOT.ML 

247 
src/Pure/Pure.thy 

248 
src/Pure/ML_Bootstrap.thy 

249 

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

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

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

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

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

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

63307  256 
dependencies of the above files are only observed for batch build. 
62904  257 

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

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

63461  261 

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

265 
new 'abbrevs' section. 

266 

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

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

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

63579  270 

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

273 
keymap; nonconflicting changes are always applied implicitly. This 

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

275 
increases chances that users see new keyboard shortcuts when reusing 

276 
old keymaps. 

277 

63675  278 
* ML and document antiquotations for filesystems paths are more uniform 
279 
and diverse: 

280 

281 
@{path NAME}  no filesystem check 

282 
@{file NAME}  check for plain file 

283 
@{dir NAME}  check for directory 

284 

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

286 
have to be changed. 

63669  287 

288 

63977  289 
*** Document preparation *** 
290 

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

292 

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

295 

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

298 

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

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

301 
derivatives. 

302 

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

304 

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

306 
Isabelle2015). 

307 

308 

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

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

310 

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

313 
'definition', 'inductive', 'function'. 

314 

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

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

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

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

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

320 

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

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

63039  325 

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

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

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

328 

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

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

330 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  331 

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

334 

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

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

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

338 

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

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

341 
INCOMPATIBILITY. 

62939  342 

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

345 
definitions. 

346 

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

63259  349 

350 
(use facts in simp) 

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

352 

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

355 

62216  356 

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

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

358 

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

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

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

363 

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

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

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

367 
regardless of the actual parameters that are provided. Rare 

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

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

370 

371 
* Typeinference improves sorts of newly introduced type variables for 

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

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

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

375 
INCOMPATIBILITY, need to provide explicit type constraints for Pure 

376 
types where this is really intended. 

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

377 

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

378 

62327  379 
*** HOL *** 
380 

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

383 
propositional logic, goals based on a combination of quantifierfree 

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

385 
quantifierfree propositional logic with linear real arithmetic 

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

387 

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

390 

63977  391 
* Metis: The problem encoding has changed very slightly. This might 
63785  392 
break existing proofs. INCOMPATIBILITY. 
393 

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

395 
 The MaSh relevance filter is now faster than before. 
63116  396 
 Produce syntactically correct Vampire 4.0 problem files. 
397 

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

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

62842  402 
method. See 'isabelle doc corec'. 
63977  403 
 The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a firstclass 
63855  404 
citizen in bounded natural functors. 
62693  405 
 'primrec' now allows nested calls through the predicator in addition 
62327  406 
to the map function. 
63855  407 
 'bnf' automatically discharges reflexive proof obligations. 
62693  408 
 'bnf' outputs a slightly modified proof obligation expressing rel in 
62332  409 
terms of map and set 
63855  410 
(not giving a specification for rel makes this one reflexive). 
62693  411 
 'bnf' outputs a new proof obligation expressing pred in terms of set 
63855  412 
(not giving a specification for pred makes this one reflexive). 
413 
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. 

62335  414 
 Renamed lemmas: 
415 
rel_prod_apply ~> rel_prod_inject 

416 
pred_prod_apply ~> pred_prod_inject 

417 
INCOMPATIBILITY. 

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

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

421 
INCOMPATIBILITY. 

62327  422 

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

425 
which exposed details of the internal fixpoint construction and was 

426 
hard to use. INCOMPATIBILITY. 

427 

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

429 

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

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

432 

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

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

435 
eliminated altogether. 

436 

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

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

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

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

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

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

443 
INCOMPATIBILITY in rare situations. 

444 

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

446 
INCOMPATIBILITY. 

447 

64390  448 
* Renamed constants and corresponding theorems: 
449 

450 
setsum ~> sum 

451 
setprod ~> prod 

452 
listsum ~> sum_list 

453 
listprod ~> prod_list 

454 

455 
INCOMPATIBILITY. 

456 

457 
* Sligthly more standardized theorem names: 

458 
sgn_times ~> sgn_mult 

459 
sgn_mult' ~> Real_Vector_Spaces.sgn_mult 

460 
divide_zero_left ~> div_0 

461 
zero_mod_left ~> mod_0 

462 
divide_zero ~> div_by_0 

463 
divide_1 ~> div_by_1 

464 
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left 

465 
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left 

466 
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right 

467 
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right 

468 
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left 

469 
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right 

470 
mod_div_equality ~> div_mult_mod_eq 

471 
mod_div_equality2 ~> mult_div_mod_eq 

472 
mod_div_equality3 ~> mod_div_mult_eq 

473 
mod_div_equality4 ~> mod_mult_div_eq 

474 
minus_div_eq_mod ~> minus_div_mult_eq_mod 

475 
minus_div_eq_mod2 ~> minus_mult_div_eq_mod 

476 
minus_mod_eq_div ~> minus_mod_eq_div_mult 

477 
minus_mod_eq_div2 ~> minus_mod_eq_mult_div 

478 
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] 

479 
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] 

480 
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] 

481 
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] 

482 
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

483 
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

484 
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

485 
div_1 ~> div_by_Suc_0 

486 
mod_1 ~> mod_by_Suc_0 

487 
INCOMPATIBILITY. 

488 

489 
* New type class "idom_abs_sgn" specifies algebraic properties 

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

491 
disappeared. Slight INCOMPATIBILITY. 

492 

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

494 

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

497 

498 
 Logical representation: 

499 
* 0 is instantiated to the ASCII zero character. 

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

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

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

503 
are noncanonical. 

504 
 Printing and parsing: 

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

506 
(as before). 

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

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

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

510 
is parsable for every numeral expression n. 

511 
* Noncanonical characters have no special syntax and are 

512 
printed as their logical representation. 

513 
 Explicit conversions from and to the natural numbers are 

514 
provided as char_of_nat, nat_of_char (as before). 

515 
 The auxiliary nibble type has been discontinued. 

516 

517 
INCOMPATIBILITY. 

518 

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

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

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

522 
infix "mod" syntax. INCOMPATIBILITY. 

523 

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

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

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

528 
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY. 

529 

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

532 

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

534 
which renders those abstract effectively. 

535 

536 
* Command 'export_code' checks given constants for abstraction 

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

538 
interface for the generated code. 

539 

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

541 
spelt out explicitly. 

542 

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

544 
explicitly provided auxiliary definitions for required type class 

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

547 

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

549 
products. 

63977  550 

551 
* Locale bijection establishes convenient default simp rules such as 

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

553 

554 
* Abstract locales semigroup, abel_semigroup, semilattice, 

555 
semilattice_neutr, ordering, ordering_top, semilattice_order, 

556 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 

557 
semilattice_neutr_set, semilattice_order_set, 

558 
semilattice_order_neutr_set monoid_list, comm_monoid_list, 

559 
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified 

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

561 
INCOMPATIBILITY. 

562 

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

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

565 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

566 

63807  567 
* Some old / obsolete theorems have been renamed / removed, potential 
568 
INCOMPATIBILITY. 

569 

570 
nat_less_cases  removed, use linorder_cases instead 

571 
inv_image_comp  removed, use image_inv_f_f instead 

572 
image_surj_f_inv_f ~> image_f_inv_f 

63113  573 

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

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

575 
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

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

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

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

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

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

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

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

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

584 

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

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

586 
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

587 
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

588 
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

589 
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

590 
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

591 
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

592 
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

593 
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

594 
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

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

596 

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

62396  599 

63977  600 
* Added class topological_monoid. 
601 

64391  602 
* The following theorems have been renamed: 
603 

64457  604 
setsum_left_distrib ~> sum_distrib_right 
605 
setsum_right_distrib ~> sum_distrib_left 

64391  606 

607 
INCOMPATIBILITY. 

608 

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

610 
INCOMPATIBILITY. 

611 

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

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

614 
A)". 

615 

616 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 

617 

618 
* The type class ordered_comm_monoid_add is now called 

619 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 

620 
is introduced as the combination of ordered_ab_semigroup_add + 

621 
comm_monoid_add. INCOMPATIBILITY. 

622 

623 
* Introduced the type classes canonically_ordered_comm_monoid_add and 

624 
dioid. 

625 

626 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 

627 
instantiating linordered_semiring_strict and ordered_ab_group_add, an 

628 
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 

629 
be required. INCOMPATIBILITY. 

63117  630 

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

633 
lcm_left_commute_nat ~> lcm.left_commute 

634 
lcm_left_commute_int ~> lcm.left_commute 

635 
gcd_left_commute_nat ~> gcd.left_commute 

636 
gcd_left_commute_int ~> gcd.left_commute 

637 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

638 
gcd_greatest_iff_int ~> gcd_greatest_iff 

639 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

640 
coprime_dvd_mult_int ~> coprime_dvd_mult 

641 
zpower_numeral_even ~> power_numeral_even 

642 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

643 
gcd_mult_cancel_int ~> gcd_mult_cancel 

644 
div_gcd_coprime_nat ~> div_gcd_coprime 

645 
div_gcd_coprime_int ~> div_gcd_coprime 

646 
zpower_numeral_odd ~> power_numeral_odd 

647 
zero_less_int_conv ~> of_nat_0_less_iff 

648 
gcd_greatest_nat ~> gcd_greatest 

649 
gcd_greatest_int ~> gcd_greatest 

650 
coprime_mult_nat ~> coprime_mult 

651 
coprime_mult_int ~> coprime_mult 

652 
lcm_commute_nat ~> lcm.commute 

653 
lcm_commute_int ~> lcm.commute 

654 
int_less_0_conv ~> of_nat_less_0_iff 

655 
gcd_commute_nat ~> gcd.commute 

656 
gcd_commute_int ~> gcd.commute 

657 
Gcd_insert_nat ~> Gcd_insert 

658 
Gcd_insert_int ~> Gcd_insert 

659 
of_int_int_eq ~> of_int_of_nat_eq 

660 
lcm_least_nat ~> lcm_least 

661 
lcm_least_int ~> lcm_least 

662 
lcm_assoc_nat ~> lcm.assoc 

663 
lcm_assoc_int ~> lcm.assoc 

664 
int_le_0_conv ~> of_nat_le_0_iff 

665 
int_eq_0_conv ~> of_nat_eq_0_iff 

666 
Gcd_empty_nat ~> Gcd_empty 

667 
Gcd_empty_int ~> Gcd_empty 

668 
gcd_assoc_nat ~> gcd.assoc 

669 
gcd_assoc_int ~> gcd.assoc 

670 
zero_zle_int ~> of_nat_0_le_iff 

671 
lcm_dvd2_nat ~> dvd_lcm2 

672 
lcm_dvd2_int ~> dvd_lcm2 

673 
lcm_dvd1_nat ~> dvd_lcm1 

674 
lcm_dvd1_int ~> dvd_lcm1 

675 
gcd_zero_nat ~> gcd_eq_0_iff 

676 
gcd_zero_int ~> gcd_eq_0_iff 

677 
gcd_dvd2_nat ~> gcd_dvd2 

678 
gcd_dvd2_int ~> gcd_dvd2 

679 
gcd_dvd1_nat ~> gcd_dvd1 

680 
gcd_dvd1_int ~> gcd_dvd1 

681 
int_numeral ~> of_nat_numeral 

682 
lcm_ac_nat ~> ac_simps 

683 
lcm_ac_int ~> ac_simps 

684 
gcd_ac_nat ~> ac_simps 

685 
gcd_ac_int ~> ac_simps 

686 
abs_int_eq ~> abs_of_nat 

687 
zless_int ~> of_nat_less_iff 

688 
zdiff_int ~> of_nat_diff 

689 
zadd_int ~> of_nat_add 

690 
int_mult ~> of_nat_mult 

691 
int_Suc ~> of_nat_Suc 

692 
inj_int ~> inj_of_nat 

693 
int_1 ~> of_nat_1 

694 
int_0 ~> of_nat_0 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

717 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  718 
realpow_minus_mult ~> power_minus_mult 
719 
realpow_Suc_le_self ~> power_Suc_le_self 

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

720 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  721 
INCOMPATIBILITY. 
722 

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

723 
* Renamed HOL/Quotient_Examples/FSet.thy to 
63977  724 
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. 
725 

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

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

729 
"unbundle finfun_syntax" to imitate import of 

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

731 

732 
* Session HOLLibrary: theory Multiset_Permutations (executably) defines 

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

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

735 
once. 

736 

737 
* Session HOLLibrary: multiset membership is now expressed using 

738 
set_mset rather than count. 

739 

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

741 
by default. 

742 

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

744 
equations count_eq_zero_iff and not_in_iff. 

745 

746 
 Rules count_inI and in_countE obtain facts of the form 

747 
"count M a = n" from membership. 

748 

749 
 Rules count_in_diffI and in_diff_countE obtain facts of the form 

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

751 

752 
INCOMPATIBILITY. 

753 

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

755 
displaying equations in functional programming style  variables 

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

757 
underscores. 

758 

759 
* Session HOLLibrary: theory Combinator_PER provides combinator to 

760 
build partial equivalence relations from a predicate and an equivalence 

761 
relation. 

762 

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

764 
everywhere fix bijections. 

765 

766 
* Session HOLLibrary: theory Normalized_Fraction allows viewing an 

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

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

769 
denominator is normalized wrt. unit factors). 

770 

771 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 

772 

773 
* Session HOLMultivariate_Analysis has been renamed to HOLAnalysis. 

774 

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

776 
HOLProbability. When importing HOLAnalysis some theorems need 

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

778 

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

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

781 
principle, Residue theorem, Schwarz Lemma. 

782 

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

784 
polytopes, and the Krein–Milman Minkowski theorem. 

785 

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

787 
libraries: homeomorphisms, continuous function extensions, invariance of 

788 
domain. 

789 

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

791 
changed from ereal to ennreal, INCOMPATIBILITY. 

792 

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

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

795 

796 
* Session HOLProbability: Code generation and QuickCheck for 

797 
Probability Mass Functions. 

798 

799 
* Session HOLProbability: theory Random_Permutations contains some 

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

801 
folding over a list in random order. 

802 

803 
* Session HOLProbability: theory SPMF formalises discrete 

804 
subprobability distributions. 

805 

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

807 
normalised to distinguish which ordering the theorems are about 

808 

809 
mset_less_eqI ~> mset_subset_eqI 

810 
mset_less_insertD ~> mset_subset_insertD 

811 
mset_less_eq_count ~> mset_subset_eq_count 

812 
mset_less_diff_self ~> mset_subset_diff_self 

813 
mset_le_exists_conv ~> mset_subset_eq_exists_conv 

814 
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel 

815 
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel 

816 
mset_le_mono_add ~> mset_subset_eq_mono_add 

817 
mset_le_add_left ~> mset_subset_eq_add_left 

818 
mset_le_add_right ~> mset_subset_eq_add_right 

819 
mset_le_single ~> mset_subset_eq_single 

820 
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute 

821 
diff_le_self ~> diff_subset_eq_self 

822 
mset_leD ~> mset_subset_eqD 

823 
mset_lessD ~> mset_subsetD 

824 
mset_le_insertD ~> mset_subset_eq_insertD 

825 
mset_less_of_empty ~> mset_subset_of_empty 

826 
mset_less_size ~> mset_subset_size 

827 
wf_less_mset_rel ~> wf_subset_mset_rel 

828 
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq 

829 
mset_remdups_le ~> mset_remdups_subset_eq 

830 
ms_lesseq_impl ~> subset_eq_mset_impl 

831 

832 
Some functions have been renamed: 

833 
ms_lesseq_impl > subset_eq_mset_impl 

834 

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

836 
#\<subseteq># ~> \<le> 

837 
#\<subset># ~> < 

838 
le_multiset ~> less_eq_multiset 

839 
less_multiset ~> le_multiset 

840 
INCOMPATIBILITY. 

841 

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

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

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

845 
interpretations "multiset_linorder" and "multiset_wellorder" have been 

846 
replaced by instantiations. INCOMPATIBILITY. 

847 

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

849 
been renamed: 

850 

851 
le_multiset_def ~> less_eq_multiset_def 

852 
less_multiset_def ~> le_multiset_def 

853 
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset 

854 
mult_less_not_refl ~> mset_le_not_refl 

855 
mult_less_trans ~> mset_le_trans 

856 
mult_less_not_sym ~> mset_le_not_sym 

857 
mult_less_asym ~> mset_le_asym 

858 
mult_less_irrefl ~> mset_le_irrefl 

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

860 

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

862 
le_multiset_total ~> less_eq_multiset_total 

863 
less_multiset_right_total ~> subset_eq_imp_le_multiset 

864 
le_multiset_empty_left ~> less_eq_multiset_empty_left 

865 
le_multiset_empty_right ~> less_eq_multiset_empty_right 

866 
less_multiset_empty_right ~> le_multiset_empty_left 

867 
less_multiset_empty_left ~> le_multiset_empty_right 

868 
union_less_diff_plus ~> union_le_diff_plus 

869 
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset 

870 
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty 

871 
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty 

872 
INCOMPATIBILITY. 

873 

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

875 
INCOMPATIBILITY. 

876 

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

878 
INCOMPATIBILITY, use the following replacements: 

879 

880 
le_multiset_plus_plus_left_iff ~> add_less_cancel_right 

881 
less_multiset_plus_plus_left_iff ~> add_less_cancel_right 

882 
le_multiset_plus_plus_right_iff ~> add_less_cancel_left 

883 
less_multiset_plus_plus_right_iff ~> add_less_cancel_left 

884 
add_eq_self_empty_iff ~> add_cancel_left_right 

885 
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right 

886 
mset_less_add_bothsides ~> subset_mset.add_less_cancel_right 

887 
mset_le_add_bothsides ~> subset_mset.add_less_cancel_right 

888 
empty_inter ~> subset_mset.inf_bot_left 

889 
inter_empty ~> subset_mset.inf_bot_right 

890 
empty_sup ~> subset_mset.sup_bot_left 

891 
sup_empty ~> subset_mset.sup_bot_right 

892 
bdd_below_multiset ~> subset_mset.bdd_above_bot 

893 
subset_eq_empty ~> subset_mset.le_zero_eq 

894 
le_empty ~> subset_mset.le_zero_eq 

895 
mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

896 
mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

897 

898 
* Session HOLLibrary: some typeclass constraints about multisets have 

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

900 
additional typeclasses order_bot, no_top, 

901 
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, 

902 
linordered_cancel_ab_semigroup_add, and 

903 
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. 

904 

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

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

907 
INCOMPATIBILITY. 

908 

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

910 
interpretations ordered_ab_semigroup_monoid_add_imp_le and 

911 
bounded_lattice_bot. INCOMPATIBILITY. 

912 

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

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

915 
removed or changed: 

916 

917 
single_not_empty ~> add_mset_not_empty or empty_not_add_mset 

918 
fold_mset_insert ~> fold_mset_add_mset 

919 
image_mset_insert ~> image_mset_add_mset 

920 
union_single_eq_diff 

921 
multi_self_add_other_not_self 

922 
diff_single_eq_union 

923 
INCOMPATIBILITY. 

924 

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

926 
to use add_mset instead of single: 

927 

928 
mset_add 

929 
multi_self_add_other_not_self 

930 
diff_single_eq_union 

931 
union_single_eq_diff 

932 
union_single_eq_member 

933 
add_eq_conv_diff 

934 
insert_noteq_member 

935 
add_eq_conv_ex 

936 
multi_member_split 

937 
multiset_add_sub_el_shuffle 

938 
mset_subset_eq_insertD 

939 
mset_subset_insertD 

940 
insert_subset_eq_iff 

941 
insert_union_subset_iff 

942 
multi_psub_of_add_self 

943 
inter_add_left1 

944 
inter_add_left2 

945 
inter_add_right1 

946 
inter_add_right2 

947 
sup_union_left1 

948 
sup_union_left2 

949 
sup_union_right1 

950 
sup_union_right2 

951 
size_eq_Suc_imp_eq_union 

952 
multi_nonempty_split 

953 
mset_insort 

954 
mset_update 

955 
mult1I 

956 
less_add 

957 
mset_zip_take_Cons_drop_twice 

958 
rel_mset_Zero 

959 
msed_map_invL 

960 
msed_map_invR 

961 
msed_rel_invL 

962 
msed_rel_invR 

963 
le_multiset_right_total 

964 
multiset_induct 

965 
multiset_induct2_size 

966 
multiset_induct2 

967 
INCOMPATIBILITY. 

968 

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

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

971 
element: 

972 

973 
image_mset 

974 
mset 

975 
replicate_mset 

976 
mult1 

977 
pred_mset 

978 
rel_mset' 

979 
mset_insort 

980 

981 
INCOMPATIBILITY. 

982 

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

984 
attributes of some multiset theorems have been changed: 

985 

986 
insert_DiffM [] ~> [simp] 

987 
insert_DiffM2 [simp] ~> [] 

988 
diff_add_mset_swap [simp] 

989 
fold_mset_add_mset [simp] 

990 
diff_diff_add [simp] (for multisets only) 

991 
diff_cancel [simp] ~> [] 

992 
count_single [simp] ~> [] 

993 
set_mset_single [simp] ~> [] 

994 
size_multiset_single [simp] ~> [] 

995 
size_single [simp] ~> [] 

996 
image_mset_single [simp] ~> [] 

997 
mset_subset_eq_mono_add_right_cancel [simp] ~> [] 

998 
mset_subset_eq_mono_add_left_cancel [simp] ~> [] 

999 
fold_mset_single [simp] ~> [] 

1000 
subset_eq_empty [simp] ~> [] 

1001 
empty_sup [simp] ~> [] 

1002 
sup_empty [simp] ~> [] 

1003 
inter_empty [simp] ~> [] 

1004 
empty_inter [simp] ~> [] 

1005 
INCOMPATIBILITY. 

1006 

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

1010 
INCOMPATIBILITY. 

1011 

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

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

1014 
natural numbers. INCOMPATIBILITY. 

1015 

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

1017 
multisets: 

1018 

1019 
msetsum ~> sum_mset 

1020 
msetprod ~> prod_mset 

1021 

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

1023 
and union of multisets have been changed: 

1024 

1025 
#\<inter> ~> \<inter># 

1026 
#\<union> ~> \<union># 

1027 

1028 
INCOMPATIBILITY. 

1029 

1030 
* Session HOLLibrary, theory Multiset: the lemma 

1031 
one_step_implies_mult_aux on multisets has been removed, use 

1032 
one_step_implies_mult instead. INCOMPATIBILITY. 

1033 

1034 
* Session HOLLibrary: theory Complete_Partial_Order2 provides reasoning 

1035 
support for monotonicity and continuity in chaincomplete partial orders 

1036 
and about admissibility conditions for fixpoint inductions. 

1037 

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

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

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

1042 
future different type class instantiation for polynomials over factorial 

1043 
rings. INCOMPATIBILITY. 

64390  1044 

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

1046 
the following renaming 

1047 

1048 
prefixeq > prefix 

1049 
prefix > strict_prefix 

1050 
suffixeq > suffix 

1051 
suffix > strict_suffix 

1052 

1053 
Added theory of longest common prefixes. 

64389  1054 

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

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

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

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

1060 
"prime_nat_iff". INCOMPATIBILITY. 

1061 

1062 
* Session Old_Number_Theory has been removed, after porting remaining 

1063 
theories. 

1064 

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

1067 

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

1068 

62498  1069 
*** ML *** 
1070 

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

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

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

1075 
INCOMPATIBILITY. 

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

1076 

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

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

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

1084 

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

1087 

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

1089 
with approximative output quality. 

1090 

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

1092 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 

1093 

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

1096 
requiring separate files. 

1097 

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

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

1101 
debugger information requires consirable time and space: main 

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

1103 

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

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

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

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

1109 
balanced blocks of Local_Theory.open_target versus 

1110 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

1111 

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

1114 
INCOMPATIBILITY. 

1115 

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

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

1119 
File.full_path). Potential INCOMPATIBILITY. 

1120 

63352  1121 
* Binding.empty_atts supersedes Thm.empty_binding and 
1122 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

1123 

62498  1124 

62354  1125 
*** System *** 
1126 

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

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

1130 
much less disk space. 

63226  1131 

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

1134 
particular: 

1135 

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

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

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

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

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

1140 

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

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

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

1144 

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

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

1146 
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

1147 
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

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

1149 

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

1152 
servers with separate CPU/memory modules. 

1153 

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

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

64274  1156 
unless there is already a default provided via ML_OPTIONS settings. 
1157 

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

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

1159 
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

1160 
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

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

1162 

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

1166 
resulting log files. 

64308  1167 

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

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

1169 
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

1170 
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

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

1172 

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

1175 

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

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

1178 
Isabelle/ML or Isabelle/Scala. 

1179 

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

1181 
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, 

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

1183 
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been 

1184 
discontinued. Potential INCOMPATIBILITY. 

1185 

1186 
* The Isabelle system environment always ensures that the main 

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

1188 
"isabelle_scala_script". 

1189 

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

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

1192 
Isabelle_Tool.Body. 

1193 

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

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

1196 
produce robust shell scripts under program control, without worrying 

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

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

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

1200 
been discontinued. 

1201 

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

1204 
but without the Isabelle settings environment. 

1205 

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

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

1209 
that Path specifications need to be resolved remotely via 

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

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

1212 

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

1214 
regular hg commandline interface. The repositroy clone and working 

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

1216 
connection). 

64265  1217 

62354  1218 

1219 

62031  1220 
New in Isabelle2016 (February 2016) 
62016  1221 
 
60138  1222 

61337  1223 
*** General *** 
1224 

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

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

1226 
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

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

1228 
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

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

1230 

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

1233 

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

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

1237 
has been removed (see below). 

1238 

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

62017  1241 

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

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

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

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

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

1246 

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

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

1248 
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

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

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

1251 

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

1254 
to update old sources. 

1255 

61337  1256 
* Toplevel theorem statements have been simplified as follows: 
1257 

1258 
theorems ~> lemmas 

1259 
schematic_lemma ~> schematic_goal 

1260 
schematic_theorem ~> schematic_goal 

1261 
schematic_corollary ~> schematic_goal 

1262 

1263 
Commandline tool "isabelle update_theorems" updates theory sources 

1264 
accordingly. 

1265 

61338  1266 
* Toplevel theorem statement 'proposition' is another alias for 
1267 
'theorem'. 

1268 

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

1271 
deferred definitions require a surrounding 'overloading' block. 

1272 

61337  1273 

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

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

1275 

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

1279 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

1283 
any effect on the running ML program. 

60984  1284 

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

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

1288 
update. 

61729  1289 

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

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

1292 
enable option "editor_output_state". 

61215  1293 

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

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

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

1298 
visibility. 

1299 

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

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

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

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

1304 
panel. 

1305 

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

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

1307 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1308 

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

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

1311 
implicit: a popup will show up unconditionally. 

1312 

1313 
* Additional abbreviations for syntactic completion may be specified in 

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

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

1316 

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

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

1318 
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

1319 
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

1320 
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

1321 

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

1324 
the editor. 

1325 

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

1327 
instead of former C+e LEFT. 

1328 

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

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

1331 
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

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

1333 

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

1336 
singleinstance applications seen on common GUI desktops. 

1337 

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

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

1339 
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

1340 
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

1341 

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

1344 

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

1347 

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

1348 

61405  1349 
*** Document preparation *** 
1350 

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

1353 

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

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

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

1357 

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

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

1360 
follows: 

1361 

1362 
\<^item> itemize 

1363 
\<^enum> enumerate 

1364 
\<^descr> description 

1365 

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

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

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

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

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

1372 

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

1375 
standard LaTeX macros of the same names. 

1376 

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

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

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

1381 
cartouche tokens seen in theory sources. 

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

1382 

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

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

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

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

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

1388 

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

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

1392 

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

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

1395 

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

1397 

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

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

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

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

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

1403 
documentation, with a hyperlink in the Prover IDE. 

1404 

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

1406 
entities of the Isar language. 

1407 

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

61488  1410 
print mode "HTML" loses its special meaning. 
61471  1411 

61405  1412 

60406  1413 
*** Isar *** 
1414 

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

1417 
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

1418 
example: 
60414  1419 

1420 
have result: "C x y" 

1421 
if "A x" and "B y" 

1422 
for x :: 'a and y :: 'a 

1423 
<proof> 

1424 

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

60414  1427 
corresponds to a raw proof block like this: 
1428 

1429 
{ 

1430 
fix x :: 'a and y :: 'a 

60449  1431 
assume that: "A x" "B y" 
60414  1432 
have "C x y" <proof> 