author  haftmann 
Tue, 13 Oct 2015 09:21:15 +0200  
changeset 61424  c3658c18b7bc 
parent 61405  d2ce32c5793a 
child 61426  d53db136e8fd 
permissions  rwrr 
57491  1 
Isabelle NEWS  history of userrelevant changes 
2 
================================================= 

2553  3 

60007  4 
(Note: Isabelle/jEdit shows a treeview of this file in Sidekick.) 
5 

60331  6 

60138  7 
New in this Isabelle version 
8 
 

9 

61337  10 
*** General *** 
11 

12 
* Toplevel theorem statements have been simplified as follows: 

13 

14 
theorems ~> lemmas 

15 
schematic_lemma ~> schematic_goal 

16 
schematic_theorem ~> schematic_goal 

17 
schematic_corollary ~> schematic_goal 

18 

19 
Commandline tool "isabelle update_theorems" updates theory sources 

20 
accordingly. 

21 

61338  22 
* Toplevel theorem statement 'proposition' is another alias for 
23 
'theorem'. 

24 

61380  25 
* HTML presentation uses the standard IsabelleText font and Unicode 
26 
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former 

27 
print mode "HTML" looses its special meaning. 

28 

61337  29 

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

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

31 

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

32 
* Improved scheduling for urgent print tasks (e.g. command state output, 
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

33 
interactive queries) wrt. longrunning background tasks. 
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

34 

60986  35 
* IDE support for the sourcelevel debugger of Poly/ML, to work with 
60984  36 
Isabelle/ML and official Standard ML. Configuration option "ML_debugger" 
37 
and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', 

38 
'SML_file_no_debug' control compilation of sources with debugging 

39 
information. The Debugger panel allows to set breakpoints (via context 

40 
menu), step through stopped threads, evaluate local ML expressions etc. 

41 
At least one Debugger view needs to be active to have any effect on the 

42 
running ML program. 

43 

61173  44 
* The main Isabelle executable is managed as singleinstance Desktop 
45 
application uniformly on all platforms: Linux, Windows, Mac OS X. 

61170  46 

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

49 
full document node content is taken into account. 

50 

61218  51 
* The State panel manages explicit proof state output, with jEdit action 
52 
"isabelle.updatestate" (shortcut S+ENTER) to trigger update according 

53 
to cursor position. Option "editor_output_state" controls implicit proof 

54 
state output in the Output panel: suppressing this reduces resource 

55 
requirements of prover time and GUI space. 

61215  56 

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

57 

61405  58 
*** Document preparation *** 
59 

60 
* Isabelle control symbols for markup and formatting: 

61 

62 
\<^smallskip> \smallskip 

63 
\<^medskip> \medskip 

64 
\<^bigskip> \bigskip 

65 

66 
\<^item> \item (itemize) 

67 
\<^enum> \item (enumeration) 

68 

69 

60406  70 
*** Isar *** 
71 

72 
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the 

73 
proof body as well, abstracted over relevant parameters. 

74 

60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60460
diff
changeset

75 
* Improved typeinference for theorem statement 'obtains': separate 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60460
diff
changeset

76 
parameter scope for of each clause. 
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60460
diff
changeset

77 

60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60406
diff
changeset

78 
* Term abbreviations via 'is' patterns also work for schematic 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60406
diff
changeset

79 
statements: result is abstracted over unknowns. 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60406
diff
changeset

80 

60414  81 
* Local goals ('have', 'show', 'hence', 'thus') allow structured 
82 
statements like fixes/assumes/shows in theorem specifications, but the 

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

83 
notation is postfix with keywords 'if' (or 'when') and 'for'. For 
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

84 
example: 
60414  85 

86 
have result: "C x y" 

87 
if "A x" and "B y" 

88 
for x :: 'a and y :: 'a 

89 
<proof> 

90 

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

60414  93 
corresponds to a raw proof block like this: 
94 

95 
{ 

96 
fix x :: 'a and y :: 'a 

60449  97 
assume that: "A x" "B y" 
60414  98 
have "C x y" <proof> 
99 
} 

100 
note result = this 

60406  101 

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

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

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

104 

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

107 
a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows: 

108 

109 
show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" 

110 

111 
or: 

112 

113 
show "C x" if "A x" "B x" for x 

114 

115 
Rare INCOMPATIBILITY, the old behaviour may be recovered as follows: 

116 

117 
show "C x" when "A x" "B x" for x 

118 

60406  119 
* New command 'supply' supports fact definitions during goal refinement 
120 
('apply' scripts). 

121 

60459  122 
* New command 'consider' states rules for generalized elimination and 
123 
case splitting. This is like a toplevel statement "theorem obtains" used 

124 
within a proof body; or like a multibranch 'obtain' without activation 

125 
of the local context elements yet. 

126 

60455  127 
* Proof method "cases" allows to specify the rule as first entry of 
128 
chained facts. This is particularly useful with 'consider': 

129 

130 
consider (a) A  (b) B  (c) C <proof> 

131 
then have something 

132 
proof cases 

133 
case a 

134 
then show ?thesis <proof> 

135 
next 

136 
case b 

137 
then show ?thesis <proof> 

138 
next 

139 
case c 

140 
then show ?thesis <proof> 

141 
qed 

142 

60565  143 
* Command 'case' allows fact name and attribute specification like this: 
144 

145 
case a: (c xs) 

146 
case a [attributes]: (c xs) 

147 

148 
Facts that are introduced by invoking the case context are uniformly 

149 
qualified by "a"; the same name is used for the cumulative fact. The old 

150 
form "case (c xs) [attributes]" is no longer supported. Rare 

151 
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, 

152 
and always put attributes in front. 

153 

60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset

154 
* The standard proof method of commands 'proof' and '..' is now called 
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset

155 
"standard" to make semantically clear what it is; the old name "default" 
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset

156 
is still available as legacy for some time. Documentation now explains 
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset

157 
'..' more accurately as "by standard" instead of "by rule". 
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset

158 

60631  159 
* Command 'subgoal' allows to impose some structure on backward 
160 
refinements, to avoid proof scripts degenerating into long of 'apply' 

161 
sequences. Further explanations and examples are given in the isarref 

162 
manual. 

163 

61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

164 
* Proof method "goal_cases" turns the current subgoals into cases within 
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

165 
the context; the conclusion is bound to variable ?case in each case. For 
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

166 
example: 
60617  167 

168 
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" 

60622  169 
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" 
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

170 
proof goal_cases 
60622  171 
case (1 x) 
172 
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry 

173 
next 

174 
case (2 y z) 

175 
then show ?case using \<open>U y\<close> \<open>V z\<close> sorry 

176 
qed 

177 

178 
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" 

179 
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" 

61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

180 
proof goal_cases 
60617  181 
case prems: 1 
182 
then show ?case using prems sorry 

183 
next 

184 
case prems: 2 

185 
then show ?case using prems sorry 

186 
qed 

60578  187 

60581  188 
* The undocumented feature of implicit cases goal1, goal2, goal3, etc. 
60617  189 
is marked as legacy, and will be removed eventually. The proof method 
190 
"goals" achieves a similar effect within regular Isar; often it can be 

191 
done more adequately by other means (e.g. 'consider'). 

60581  192 

60551  193 
* Nesting of Isar goal structure has been clarified: the context after 
194 
the initial backwards refinement is retained for the whole proof, within 

195 
all its context sections (as indicated via 'next'). This is e.g. 

196 
relevant for 'using', 'including', 'supply': 

197 

198 
have "A \<and> A" if a: A for A 

199 
supply [simp] = a 

200 
proof 

201 
show A by simp 

202 
next 

203 
show A by simp 

204 
qed 

205 

60554  206 
* Method "sleep" succeeds after a realtime delay (in seconds). This is 
207 
occasionally useful for demonstration and testing purposes. 

208 

60406  209 

60331  210 
*** Pure *** 
211 

61252  212 
* Command 'print_definitions' prints dependencies of definitional 
213 
specifications. This functionality used to be part of 'print_theory'. 

214 

60489  215 
* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` 
216 
as well, not just "by this" or "." as before. 

217 

60331  218 
* Configuration option rule_insts_schematic has been discontinued 
219 
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 

220 

60349  221 
* Abbreviations in type classes now carry proper sort constraint. 
222 
Rare INCOMPATIBILITY in situations where the previous misbehaviour 

61228  223 
has been exploited. 
60349  224 

225 
* Refinement of userspace type system in type classes: pseudolocal 

226 
operations behave more similar to abbreviations. Potential 

227 
INCOMPATIBILITY in exotic situations. 

228 

229 

60171  230 
*** HOL *** 
231 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

232 
* Combinator to represent case distinction on products is named "case_prod", 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

233 
uniformly, discontinuing any input aliasses. Very popular theorem aliasses 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

234 
have been retained. 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

235 
Consolidated facts: 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

236 
PairE ~> prod.exhaust 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

237 
Pair_eq ~> prod.inject 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

238 
pair_collapse ~> prod.collapse 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

239 
Pair_fst_snd_eq ~> prod_eq_iff 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

240 
split_twice ~> prod.case_distrib 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

241 
split_weak_cong ~> prod.case_cong_weak 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

242 
split_split ~> prod.split 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

243 
split_split_asm ~> prod.split_asm 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

244 
splitI ~> case_prodI 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

245 
splitD ~> case_prodD 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

246 
splitI2 ~> case_prodI2 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

247 
splitI2' ~> case_prodI2' 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

248 
splitE ~> case_prodE 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

249 
splitE' ~> case_prodE' 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

250 
split_pair ~> case_prod_Pair 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

251 
split_eta ~> case_prod_eta 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

252 
split_comp ~> case_prod_comp 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

253 
mem_splitI ~> mem_case_prodI 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

254 
mem_splitI2 ~> mem_case_prodI2 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

255 
mem_splitE ~> mem_case_prodE 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

256 
The_split ~> The_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

257 
cond_split_eta ~> cond_case_prod_eta 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

258 
Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

259 
Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

260 
in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

261 
Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

262 
Collect_split_Grp_inD ~> Collect_case_prod_Grp_in 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

263 
Domain_Collect_split ~> Domain_Collect_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

264 
Image_Collect_split ~> Image_Collect_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

265 
Range_Collect_split ~> Range_Collect_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

266 
Eps_split ~> Eps_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

267 
Eps_split_eq ~> Eps_case_prod_eq 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

268 
split_rsp ~> case_prod_rsp 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

269 
curry_split ~> curry_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

270 
split_curry ~> case_prod_curry 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

271 
Changes in structure HOLogic: 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

272 
split_const ~> case_prod_const 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

273 
mk_split ~> mk_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

274 
mk_psplits ~> mk_ptupleabs 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

275 
strip_psplits ~> strip_ptupleabs 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

276 
INCOMPATIBILITY. 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

277 

61308  278 
* Commands 'inductive' and 'inductive_set' work better when names for 
279 
intro rules are omitted: the "cases" and "induct" rules no longer 

280 
declare empty case_names, but no case_names at all. This allows to use 

281 
numbered cases in proofs, without requiring method "goal_cases". 

282 

61269
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset

283 
* The 'typedef' command has been upgraded from a partially checked 
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset

284 
"axiomatization", to a full definitional specification that takes the 
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset

285 
global collection of overloaded constant / type definitions into 
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset

286 
account. Type definitions with open dependencies on overloaded 
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset

287 
definitions need to be specified as "typedef (overloaded)". This 
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset

288 
provides extra robustness in theory construction. Rare INCOMPATIBILITY. 
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset

289 

61118  290 
* Qualification of various formal entities in the libraries is done more 
291 
uniformly via "context begin qualified definition ... end" instead of 

292 
oldstyle "hide_const (open) ...". Consequently, both the defined 

293 
constant and its defining fact become qualified, e.g. Option.is_none and 

294 
Option.is_none_def. Occasional INCOMPATIBILITY in applications. 

295 

61069  296 
* Some old and rarely used ASCII replacement syntax has been removed. 
297 
INCOMPATIBILITY, standard syntax with symbols should be used instead. 

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

299 
simplify porting old theories: 

300 

301 
type_notation Map.map (infixr "~=>" 0) 

302 
notation Map.map_comp (infixl "o'_m" 55) 

303 

61384  304 
type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) 
305 

306 
notation FuncSet.funcset (infixr ">" 60) 

307 
notation FuncSet.extensional_funcset (infixr ">\<^sub>E" 60) 

308 

309 
notation Omega_Words_Fun.conc (infixr "conc" 65) 

310 

311 
notation Preorder.equiv ("op ~~") 

312 
and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) 

313 

61143  314 
* The alternative notation "\<Colon>" for type and sort constraints has been 
315 
removed: in LaTeX document output it looks the same as "::". 

316 
INCOMPATIBILITY, use plain "::" instead. 

317 

60841  318 
* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has 
319 
been removed. INCOMPATIBILITY. 

320 

60712
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset

321 
* Quickcheck setup for finite sets. 
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset

322 

60171  323 
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY. 
60138  324 

60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

325 
* Sledgehammer: 
61318  326 
 The MaSh relevance filter has been sped up. 
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

327 
 Proof reconstruction has been improved, to minimize the incidence of 
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

328 
cases where Sledgehammer gives a proof that does not work. 
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

329 
 Auto Sledgehammer now minimizes and preplays the results. 
61030  330 
 Handle Vampire 4.0 proof output without raising exception. 
61043  331 
 Eliminated "MASH" environment variable. Use the "MaSh" option in 
332 
Isabelle/jEdit instead. INCOMPATIBILITY. 

61317  333 
 Eliminated obsolete "blocking" option and related subcommands. 
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

334 

60310  335 
* Nitpick: 
61325
1cfc476198c9
avoid too aggressive optimization of 'finite' predicate
blanchet
parents:
61324
diff
changeset

336 
 Fixed soundness bug in translation of "finite" predicate. 
61324
d4ec7594f558
avoid unsound simplification of (C (s x)) when s is a selector but not C's
blanchet
parents:
61318
diff
changeset

337 
 Fixed soundness bug in "destroy_constrs" optimization. 
60310  338 
 Removed "check_potential" and "check_genuine" options. 
61317  339 
 Eliminated obsolete "blocking" option. 
60310  340 

61345  341 
* New (co)datatype package: 
342 
 New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF 

343 
structure on the raw type to an abstract type defined using typedef. 

344 
 Always generate "case_transfer" theorem. 

60920  345 

61370  346 
* Transfer: 
347 
 new methods for interactive debugging of 'transfer' and 

348 
'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end', 

349 
'transfer_prover_start' and 'transfer_prover_end'. 

350 

60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset

351 
* Division on integers is bootstrapped directly from division on 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset

352 
naturals and uses generic numeral algorithm for computations. 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset

353 
Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset

354 
former simprocs binary_int_div and binary_int_mod 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset

355 

60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset

356 
* Tightened specification of class semiring_no_zero_divisors. Slight 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset

357 
INCOMPATIBILITY. 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset

358 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

359 
* Class algebraic_semidom introduces common algebraic notions of 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

360 
integral (semi)domains, particularly units. Although 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

361 
logically subsumed by fields, is is not a super class of these 
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

362 
in order not to burden fields with notions that are trivial there. 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

363 

01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

364 
* Class normalization_semidom specifies canonical representants 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

365 
for equivalence classes of associated elements in an integral 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

366 
(semi)domain. This formalizes associated elements as well. 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

367 

01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

368 
* Abstract specification of gcd/lcm operations in classes semiring_gcd, 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

369 
semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

370 
and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

371 
and gcd_int.assoc by gcd.assoc. 
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset

372 

60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset

373 
* Former constants Fields.divide (_ / _) and Divides.div (_ div _) 
60354
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
60349
diff
changeset

374 
are logically unified to Rings.divide in syntactic type class 
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset

375 
Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) 
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset

376 
for field division is added later as abbreviation in class Fields.inverse. 
60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset

377 
INCOMPATIBILITY, instantiations must refer to Rings.divide rather 
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset

378 
than the former separate constants, hence infix syntax (_ / _) is usually 
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset

379 
not available during instantiation. 
60354
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
60349
diff
changeset

380 

60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

381 
* Library/Multiset: 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

382 
 Renamed multiset inclusion operators: 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

383 
< ~> <# 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

384 
\<subset> ~> \<subset># 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

385 
<= ~> <=# 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

386 
\<le> ~> \<le># 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

387 
\<subseteq> ~> \<subseteq># 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

388 
INCOMPATIBILITY. 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

389 
 "'a multiset" is no longer an instance of the "order", 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

390 
"ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff", 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

391 
"semilattice_inf", and "semilattice_sup" type classes. The theorems 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

392 
previously provided by these type classes (directly or indirectly) 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

393 
are now available through the "subset_mset" interpretation 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

394 
(e.g. add_mono ~> subset_mset.add_mono). 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

395 
INCOMPATIBILITY. 
60497  396 
 Renamed conversions: 
60515  397 
multiset_of ~> mset 
398 
multiset_of_set ~> mset_set 

60497  399 
set_of ~> set_mset 
400 
INCOMPATIBILITY 

60398  401 
 Renamed lemmas: 
402 
mset_le_def ~> subseteq_mset_def 

403 
mset_less_def ~> subset_mset_def 

60400  404 
less_eq_multiset.rep_eq ~> subseteq_mset_def 
405 
INCOMPATIBILITY 

406 
 Removed lemmas generated by lift_definition: 

407 
less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer 

408 
less_eq_multiset_def 

409 
INCOMPATIBILITY 

60007  410 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60802
diff
changeset

411 
* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem, 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60802
diff
changeset

412 
ported from HOL Light 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60802
diff
changeset

413 

60523  414 
* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' 
415 
command. Minor INCOMPATIBILITY, use 'function' instead. 

416 

61121
efe8b18306b7
do not expose lowlevel "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset

417 
* Recursive function definitions ('fun', 'function', 'partial_function') 
efe8b18306b7
do not expose lowlevel "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset

418 
no longer expose the lowlevel "_def" facts of the internal 
efe8b18306b7
do not expose lowlevel "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset

419 
construction. INCOMPATIBILITY, enable option "function_defs" in the 
efe8b18306b7
do not expose lowlevel "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset

420 
context for rare situations where these facts are really needed. 
efe8b18306b7
do not expose lowlevel "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset

421 

61119  422 
* Imperative_HOL: obsolete theory Legacy_Mrec has been removed. 
423 

61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
61174
diff
changeset

424 
* Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a. 
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
61174
diff
changeset

425 

60479  426 

60793  427 
*** ML *** 
428 

61268  429 
* The auxiliary module Pure/display.ML has been eliminated. Its 
430 
elementary thm print operations are now in Pure/more_thm.ML and thus 

431 
called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. 

432 

61144  433 
* Simproc programming interfaces have been simplified: 
434 
Simplifier.make_simproc and Simplifier.define_simproc supersede various 

435 
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that 

436 
term patterns for the lefthand sides are specified with implicitly 

437 
fixed variables, like toplevel theorem statements. INCOMPATIBILITY. 

438 

60802  439 
* Instantiation rules have been reorganized as follows: 
440 

441 
Thm.instantiate (*lowlevel instantiation with named arguments*) 

442 
Thm.instantiate' (*version with positional arguments*) 

443 

444 
Drule.infer_instantiate (*instantiation with type inference*) 

445 
Drule.infer_instantiate' (*version with positional arguments*) 

446 

447 
The LHS only requires variable specifications, instead of full terms. 

448 
Old cterm_instantiate is superseded by infer_instantiate. 

449 
INCOMPATIBILITY, need to readjust some ML names and types accordingly. 

450 

60793  451 
* Old tactic shorthands atac, rtac, etac, dtac, ftac have been 
452 
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc. 

453 
instead (with proper context). 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

454 

48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

455 
* Thm.instantiate (and derivatives) no longer require the LHS of the 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

456 
instantiation to be certified: plain variables are given directly. 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

457 

60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

458 
* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

459 
quasibound variables (like the Simplifier), instead of accidentally 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

460 
named local fixes. This has the potential to improve stability of proof 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

461 
tools, but can also cause INCOMPATIBILITY for tools that don't observe 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

462 
the proof context discipline. 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

463 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

464 

60983
ff4a67c65084
updated to polyml5.5.320150820, with native x86windows support;
wenzelm
parents:
60922
diff
changeset

465 
*** System *** 
ff4a67c65084
updated to polyml5.5.320150820, with native x86windows support;
wenzelm
parents:
60922
diff
changeset

466 

61174  467 
* Property values in etc/symbols may contain spaces, if written with the 
468 
replacement character "␣" (Unicode point 0x2324). For example: 

469 

470 
\<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono 

471 

61173  472 
* Commandline tool "isabelle jedit_client" allows to connect to already 
473 
running Isabelle/jEdit process. This achieves the effect of 

474 
singleinstance applications seen on common GUI desktops. 

475 

61216  476 
* Commandline tool "isabelle update_then" expands old Isar command 
477 
conflations: 

478 

479 
hence ~> then have 

480 
thus ~> then show 

481 

482 
This syntax is more orthogonal and improves readability and 

483 
maintainability of proofs. 

484 

61158
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped offline from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset

485 
* Poly/ML default platform architecture may be changed from 32bit to 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped offline from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset

486 
64bit via system option ML_system_64. A system restart (and rebuild) 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped offline from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset

487 
is required after change. 
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped offline from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset

488 

61074  489 
* Poly/ML 5.5.3 runs natively on x86windows and x86_64windows, 
490 
which both allow larger heap space than former x86cygwin. 

60983
ff4a67c65084
updated to polyml5.5.320150820, with native x86windows support;
wenzelm
parents:
60922
diff
changeset

491 

60996
5176de8f90db
updated to jdk8u60, with support for x86_64windows;
wenzelm
parents:
60986
diff
changeset

492 
* Java runtime environment for x86_64windows allows to use larger heap 
5176de8f90db
updated to jdk8u60, with support for x86_64windows;
wenzelm
parents:
60986
diff
changeset

493 
space. 
5176de8f90db
updated to jdk8u60, with support for x86_64windows;
wenzelm
parents:
60986
diff
changeset

494 

61135
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

495 
* Java runtime options are determined separately for 32bit vs. 64bit 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

496 
platforms as follows. 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

497 

8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

498 
 Isabelle desktop application: platformspecific files that are 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

499 
associated with the main app bundle 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

500 

8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

501 
 isabelle jedit: settings 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

502 
JEDIT_JAVA_SYSTEM_OPTIONS 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

503 
JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

504 

8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

505 
 isabelle build: settings 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

506 
ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

507 

61294  508 
* Bash shell function "jvmpath" has been renamed to "platform_path": it 
509 
is relevant both for Poly/ML and JVM processes. 

510 

60983
ff4a67c65084
updated to polyml5.5.320150820, with native x86windows support;
wenzelm
parents:
60922
diff
changeset

511 

60479  512 

60010  513 
New in Isabelle2015 (May 2015) 
514 
 

57695  515 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

516 
*** General *** 
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

517 

59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59936
diff
changeset

518 
* Local theory specification commands may have a 'private' or 
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset

519 
'qualified' modifier to restrict name space accesses to the local scope, 
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59936
diff
changeset

520 
as provided by some "context begin ... end" block. For example: 
59926  521 

522 
context 

523 
begin 

524 

525 
private definition ... 

526 
private lemma ... 

527 

59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset

528 
qualified definition ... 
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset

529 
qualified lemma ... 
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset

530 

59926  531 
lemma ... 
532 
theorem ... 

533 

534 
end 

535 

59901  536 
* Command 'experiment' opens an anonymous locale context with private 
537 
naming policy. 

538 

59951  539 
* Command 'notepad' requires proper nesting of begin/end and its proof 
540 
structure in the body: 'oops' is no longer supported here. Minor 

541 
INCOMPATIBILITY, use 'sorry' instead. 

542 

543 
* Command 'named_theorems' declares a dynamic fact within the context, 

544 
together with an attribute to maintain the content incrementally. This 

545 
supersedes functor Named_Thms in Isabelle/ML, but with a subtle change 

546 
of semantics due to external visual order vs. internal reverse order. 

547 

548 
* 'find_theorems': search patterns which are abstractions are 

549 
schematically expanded before search. Search results match the naive 

550 
expectation more closely, particularly wrt. abbreviations. 

551 
INCOMPATIBILITY. 

59648  552 

59569  553 
* Commands 'method_setup' and 'attribute_setup' now work within a local 
554 
theory context. 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

555 

58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset

556 
* Outer syntax commands are managed authentically within the theory 
59569  557 
context, without implicit global state. Potential for accidental 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset

558 
INCOMPATIBILITY, make sure that required theories are really imported. 
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset

559 

60116  560 
* Historical commandline terminator ";" is no longer accepted (and 
561 
already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle 

562 
update_semicolons" to remove obsolete semicolons from old theory 

563 
sources. 

564 

59951  565 
* Structural composition of proof methods (meth1; meth2) in Isar 
566 
corresponds to (tac1 THEN_ALL_NEW tac2) in ML. 

59105  567 

60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60116
diff
changeset

568 
* The Eisbach proof method language allows to define new proof methods 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60116
diff
changeset

569 
by combining existing ones with their usual syntax. The "match" proof 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60116
diff
changeset

570 
method provides basic fact/term matching in addition to 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60116
diff
changeset

571 
premise/conclusion matching through Subgoal.focus, and binds fact names 
60288
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset

572 
from matches as well as term patterns within matches. The Isabelle 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset

573 
documentation provides an entry "eisbach" for the Eisbach User Manual. 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset

574 
Sources and various examples are in ~~/src/HOL/Eisbach/. 
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60116
diff
changeset

575 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

576 

58524  577 
*** Prover IDE  Isabelle/Scala/jEdit *** 
578 

59569  579 
* Improved folding mode "isabelle" based on Isar syntax. Alternatively, 
580 
the "sidekick" mode may be used for document structure. 

581 

582 
* Extended bracket matching based on Isar language structure. System 

583 
option jedit_structure_limit determines maximum number of lines to scan 

584 
in the buffer. 

58758  585 

58540  586 
* Support for BibTeX files: context menu, contextsensitive token 
587 
marker, SideKick parser. 

58524  588 

58551  589 
* Document antiquotation @{cite} provides formal markup, which is 
60265  590 
interpreted semiformally based on .bib files that happen to be open in 
591 
the editor (hyperlinks, completion etc.). 

58551  592 

58785  593 
* Less waste of vertical space via negative line spacing (see Global 
594 
Options / Text Area). 

595 

60091
8bd5999133d4
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
wenzelm
parents:
60085
diff
changeset

596 
* Improved graphview panel with optional output of PNG or PDF, for 
60273
83de10e27007
use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
wenzelm
parents:
60265
diff
changeset

597 
display of 'thy_deps', 'class_deps' etc. 
60010  598 

60116  599 
* The commands 'thy_deps' and 'class_deps' allow optional bounds to 
600 
restrict the visualized hierarchy. 

60095  601 

60072  602 
* Improved scheduling for asynchronous print commands (e.g. provers 
603 
managed by the Sledgehammer panel) wrt. ongoing document processing. 

604 

58524  605 

59951  606 
*** Document preparation *** 
607 

608 
* Document markup commands 'chapter', 'section', 'subsection', 

609 
'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any 

610 
context, even before the initial 'theory' command. Obsolete proof 

611 
commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been 

612 
discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw' 

613 
instead. The old 'header' command is still retained for some time, but 

614 
should be replaced by 'chapter', 'section' etc. (using "isabelle 

615 
update_header"). Minor INCOMPATIBILITY. 

616 

60010  617 
* Official support for "tt" style variants, via \isatt{...} or 
618 
\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or 

619 
verbatim environment of LaTeX is no longer used. This allows @{ML} etc. 

620 
as argument to other macros (such as footnotes). 

621 

622 
* Document antiquotation @{verbatim} prints ASCII text literally in "tt" 

623 
style. 

624 

625 
* Discontinued obsolete option "document_graph": session_graph.pdf is 

626 
produced unconditionally for HTML browser_info and PDFLaTeX document. 

627 

59951  628 
* Diagnostic commands and document markup commands within a proof do not 
629 
affect the command tag for output. Thus commands like 'thm' are subject 

630 
to proof document structure, and no longer "stick out" accidentally. 

631 
Commands 'text' and 'txt' merely differ in the LaTeX style, not their 

632 
tags. Potential INCOMPATIBILITY in exotic situations. 

633 

634 
* System option "pretty_margin" is superseded by "thy_output_margin", 

635 
which is also accessible via document antiquotation option "margin". 

636 
Only the margin for document output may be changed, but not the global 

637 
pretty printing: that is 76 for plain console output, and adapted 

638 
dynamically in GUI frontends. Implementations of document 

639 
antiquotations need to observe the margin explicitly according to 

640 
Thy_Output.string_of_margin. Minor INCOMPATIBILITY. 

641 

60299
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset

642 
* Specification of 'document_files' in the session ROOT file is 
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset

643 
mandatory for document preparation. The legacy mode with implicit 
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset

644 
copying of the document/ directory is no longer supported. Minor 
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset

645 
INCOMPATIBILITY. 
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset

646 

59951  647 

58202  648 
*** Pure *** 
649 

59835
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

650 
* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

651 
etc.) allow an optional context of local variables ('for' declaration): 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

652 
these variables become schematic in the instantiated theorem; this 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

653 
behaviour is analogous to 'for' in attributes "where" and "of". 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

654 
Configuration option rule_insts_schematic (default false) controls use 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

655 
of schematic variables outside the context. Minor INCOMPATIBILITY, 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

656 
declare rule_insts_schematic = true temporarily and update to use local 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

657 
variable declarations or dummy patterns instead. 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

658 

60010  659 
* Explicit instantiation via attributes "where", "of", and proof methods 
660 
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns 

661 
("_") that stand for anonymous local variables. 

662 

59951  663 
* Generated schematic variables in standard format of exported facts are 
664 
incremented to avoid material in the proof context. Rare 

665 
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to 

666 
different index. 

667 

60011  668 
* Lexical separation of signed and unsigned numerals: categories "num" 
669 
and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence 

670 
of numeral signs, particularly in expressions involving infix syntax 

671 
like "( 1) ^ n". 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58374
diff
changeset

672 

58421  673 
* Old inner token category "xnum" has been discontinued. Potential 
674 
INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" 

675 
token category instead. 

676 

58202  677 

57737  678 
*** HOL *** 
679 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

680 
* New (co)datatype package: 
58374  681 
 The 'datatype_new' command has been renamed 'datatype'. The old 
682 
command of that name is now called 'old_datatype' and is provided 

683 
by "~~/src/HOL/Library/Old_Datatype.thy". See 

684 
'isabelle doc datatypes' for information on porting. 

685 
INCOMPATIBILITY. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

686 
 Renamed theorems: 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

687 
disc_corec ~> corec_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

688 
disc_corec_iff ~> corec_disc_iff 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

689 
disc_exclude ~> distinct_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

690 
disc_exhaust ~> exhaust_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

691 
disc_map_iff ~> map_disc_iff 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

692 
sel_corec ~> corec_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

693 
sel_exhaust ~> exhaust_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

694 
sel_map ~> map_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

695 
sel_set ~> set_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

696 
sel_split ~> split_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

697 
sel_split_asm ~> split_sel_asm 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

698 
strong_coinduct ~> coinduct_strong 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

699 
weak_case_cong ~> case_cong_weak 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

700 
INCOMPATIBILITY. 
58192  701 
 The "no_code" option to "free_constructors", "datatype_new", and 
702 
"codatatype" has been renamed "plugins del: code". 

703 
INCOMPATIBILITY. 

58044  704 
 The rules "set_empty" have been removed. They are easy 
705 
consequences of other set rules "by auto". 

706 
INCOMPATIBILITY. 

707 
 The rule "set_cases" is now registered with the "[cases set]" 

57990  708 
attribute. This can influence the behavior of the "cases" proof 
709 
method when more than one case rule is applicable (e.g., an 

710 
assumption is of the form "w : set ws" and the method "cases w" 

711 
is invoked). The solution is to specify the case rule explicitly 

712 
(e.g. "cases w rule: widget.exhaust"). 

713 
INCOMPATIBILITY. 

59675  714 
 Renamed theories: 
715 
BNF_Comp ~> BNF_Composition 

716 
BNF_FP_Base ~> BNF_Fixpoint_Base 

717 
BNF_GFP ~> BNF_Greatest_Fixpoint 

718 
BNF_LFP ~> BNF_Least_Fixpoint 

719 
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions 

720 
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions 

721 
INCOMPATIBILITY. 

60115  722 
 Lifting and Transfer setup for basic HOL types sum and prod (also 
723 
option) is now performed by the BNF package. Theories Lifting_Sum, 

724 
Lifting_Product and Lifting_Option from Main became obsolete and 

725 
were removed. Changed definitions of the relators rel_prod and 

726 
rel_sum (using inductive). 

60112  727 
INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead 
60115  728 
of rel_prod_def and rel_sum_def. 
729 
Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names 

730 
changed (e.g. map_prod_transfer ~> prod.map_transfer). 

60261  731 
 Parametricity theorems for map functions, relators, set functions, 
732 
constructors, case combinators, discriminators, selectors and 

733 
(co)recursors are automatically proved and registered as transfer 

734 
rules. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

735 

6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

736 
* Old datatype package: 
58310  737 
 The old 'datatype' command has been renamed 'old_datatype', and 
58374  738 
'rep_datatype' has been renamed 'old_rep_datatype'. They are 
739 
provided by "~~/src/HOL/Library/Old_Datatype.thy". See 

58310  740 
'isabelle doc datatypes' for information on porting. 
58374  741 
INCOMPATIBILITY. 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

742 
 Renamed theorems: 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

743 
weak_case_cong ~> case_cong_weak 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

744 
INCOMPATIBILITY. 
58374  745 
 Renamed theory: 
746 
~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy 

747 
INCOMPATIBILITY. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

748 

59039  749 
* Nitpick: 
60011  750 
 Fixed soundness bug related to the strict and nonstrict subset 
59039  751 
operations. 
752 

57737  753 
* Sledgehammer: 
59511  754 
 CVC4 is now included with Isabelle instead of CVC3 and run by 
755 
default. 

59965  756 
 Z3 is now always enabled by default, now that it is fully open 
757 
source. The "z3_non_commercial" option is discontinued. 

57737  758 
 Minimization is now always enabled by default. 
60011  759 
Removed subcommand: 
57737  760 
min 
59967  761 
 Proof reconstruction, both oneliners and Isar, has been 
59039  762 
dramatically improved. 
763 
 Improved support for CVC4 and veriT. 

57737  764 

58062  765 
* Old and new SMT modules: 
58067  766 
 The old 'smt' method has been renamed 'old_smt' and moved to 
59569  767 
'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility, 
768 
until applications have been ported to use the new 'smt' method. For 

769 
the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must 

770 
be installed, and the environment variable "OLD_Z3_SOLVER" must 

771 
point to it. 

58062  772 
INCOMPATIBILITY. 
58067  773 
 The 'smt2' method has been renamed 'smt'. 
58060  774 
INCOMPATIBILITY. 
59569  775 
 New option 'smt_reconstruction_step_timeout' to limit the 
776 
reconstruction time of Z3 proof steps in the new 'smt' method. 

59216  777 
 New option 'smt_statistics' to display statistics of the new 'smt' 
778 
method, especially runtime statistics of Z3 proof reconstruction. 

58060  779 

60261  780 
* Lifting: command 'lift_definition' allows to execute lifted constants 
781 
that have as a return type a datatype containing a subtype. This 

782 
overcomes longtime limitations in the area of code generation and 

783 
lifting, and avoids tedious workarounds. 

60258  784 

60010  785 
* Command and antiquotation "value" provide different evaluation slots 
786 
(again), where the previous strategy (NBE after ML) serves as default. 

787 
Minor INCOMPATIBILITY. 

788 

789 
* Add NO_MATCHsimproc, allows to check for syntactic nonequality. 

790 

791 
* field_simps: Use NO_MATCHsimproc for distribution rules, to avoid 

792 
nontermination in case of distributing a division. With this change 

793 
field_simps is in some cases slightly less powerful, if it fails try to 

794 
add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. 

795 

796 
* Separate class no_zero_divisors has been given up in favour of fully 

797 
algebraic semiring_no_zero_divisors. INCOMPATIBILITY. 

798 

799 
* Class linordered_semidom really requires no zero divisors. 

800 
INCOMPATIBILITY. 

801 

802 
* Classes division_ring, field and linordered_field always demand 

803 
"inverse 0 = 0". Given up separate classes division_ring_inverse_zero, 

804 
field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. 

805 

806 
* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit 

807 
additive inverse operation. INCOMPATIBILITY. 

808 

60020
065ecea354d0
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
paulson <lp15@cam.ac.uk>
parents:
60011
diff
changeset

809 
* Complex powers and square roots. The functions "ln" and "powr" are now 
60025  810 
overloaded for types real and complex, and 0 powr y = 0 by definition. 
811 
INCOMPATIBILITY: type constraints may be necessary. 

60020
065ecea354d0
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
paulson <lp15@cam.ac.uk>
parents:
60011
diff
changeset

812 

60010  813 
* The functions "sin" and "cos" are now defined for any type of sort 
814 
"{real_normed_algebra_1,banach}" type, so in particular on "real" and 

815 
"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be 

816 
needed. 

817 

818 
* New library of properties of the complex transcendental functions sin, 

819 
cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. 

820 

821 
* The factorial function, "fact", now has type "nat => 'a" (of a sort 

822 
that admits numeric types including nat, int, real and complex. 

823 
INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type 

824 
constraint, and the combination "real (fact k)" is likely to be 

825 
unsatisfactory. If a type conversion is still necessary, then use 

826 
"of_nat (fact k)" or "real_of_nat (fact k)". 

827 

828 
* Removed functions "natfloor" and "natceiling", use "nat o floor" and 

829 
"nat o ceiling" instead. A few of the lemmas have been retained and 

830 
adapted: in their names "natfloor"/"natceiling" has been replaced by 

831 
"nat_floor"/"nat_ceiling". 

832 

833 
* Qualified some duplicated fact names required for boostrapping the 

834 
type class hierarchy: 

835 
ab_add_uminus_conv_diff ~> diff_conv_add_uminus 

836 
field_inverse_zero ~> inverse_zero 

837 
field_divide_inverse ~> divide_inverse 

838 
field_inverse ~> left_inverse 

839 
Minor INCOMPATIBILITY. 

840 

841 
* Eliminated fact duplicates: 

842 
mult_less_imp_less_right ~> mult_right_less_imp_less 

843 
mult_less_imp_less_left ~> mult_left_less_imp_less 

844 
Minor INCOMPATIBILITY. 

845 

846 
* Fact consolidation: even_less_0_iff is subsumed by 

847 
double_add_less_zero_iff_single_add_less_zero (simp by default anyway). 

848 

849 
* Generalized and consolidated some theorems concerning divsibility: 

850 
dvd_reduce ~> dvd_add_triv_right_iff 

851 
dvd_plus_eq_right ~> dvd_add_right_iff 

852 
dvd_plus_eq_left ~> dvd_add_left_iff 

853 
Minor INCOMPATIBILITY. 

854 

855 
* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" 

856 
and part of theory Main. 

857 
even_def ~> even_iff_mod_2_eq_zero 

858 
INCOMPATIBILITY. 

859 

860 
* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor 

861 
INCOMPATIBILITY. 

862 

863 
* Bootstrap of listsum as special case of abstract product over lists. 

864 
Fact rename: 

865 
listsum_def ~> listsum.eq_foldr 

866 
INCOMPATIBILITY. 

867 

868 
* Product over lists via constant "listprod". 

869 

870 
* Theory List: renamed drop_Suc_conv_tl and nth_drop' to 

871 
Cons_nth_drop_Suc. 

58247
98d0f85d247f
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
nipkow
parents:
58202
diff
changeset

872 

58626  873 
* New infrastructure for compiling, running, evaluating and testing 
59569  874 
generated code in target languages in HOL/Library/Code_Test. See 
875 
HOL/Codegenerator_Test/Code_Test* for examples. 

58008  876 

60010  877 
* Library/Multiset: 
59813  878 
 Introduced "replicate_mset" operation. 
879 
 Introduced alternative characterizations of the multiset ordering in 

880 
"Library/Multiset_Order". 

59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

881 
 Renamed multiset ordering: 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

882 
<# ~> #<# 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

883 
<=# ~> #<=# 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

884 
\<subset># ~> #\<subset># 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

885 
\<subseteq># ~> #\<subseteq># 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

886 
INCOMPATIBILITY. 
59986
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset

887 
 Introduced abbreviations for illnamed multiset operations: 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset

888 
<#, \<subset># abbreviate < (strict subset) 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset

889 
<=#, \<le>#, \<subseteq># abbreviate <= (subset or equal) 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset

890 
INCOMPATIBILITY. 
59813  891 
 Renamed 
892 
in_multiset_of ~> in_multiset_in_set 

59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59991
diff
changeset

893 
Multiset.fold ~> fold_mset 
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59991
diff
changeset

894 
Multiset.filter ~> filter_mset 
59813  895 
INCOMPATIBILITY. 
59949  896 
 Removed mcard, is equal to size. 
59813  897 
 Added attributes: 
898 
image_mset.id [simp] 

899 
image_mset_id [simp] 

900 
elem_multiset_of_set [simp, intro] 

901 
comp_fun_commute_plus_mset [simp] 

902 
comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp] 

903 
in_mset_fold_plus_iff [iff] 

904 
set_of_Union_mset [simp] 

905 
in_Union_mset_iff [iff] 

906 
INCOMPATIBILITY. 

907 

60010  908 
* Library/Sum_of_Squares: simplified and improved "sos" method. Always 
909 
use local CSDP executable, which is much faster than the NEOS server. 

910 
The "sos_cert" functionality is invoked as "sos" with additional 

911 
argument. Minor INCOMPATIBILITY. 

912 

913 
* HOLDecision_Procs: New counterexample generator quickcheck 

914 
[approximation] for inequalities of transcendental functions. Uses 

915 
hardware floating point arithmetic to randomly discover potential 

60011  916 
counterexamples. Counterexamples are certified with the "approximation" 
60010  917 
method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for 
918 
examples. 

58990  919 

59354  920 
* HOLProbability: Reworked measurability prover 
60011  921 
 applies destructor rules repeatedly 
59354  922 
 removed application splitting (replaced by destructor rule) 
59569  923 
 added congruence rules to rewrite measure spaces under the sets 
924 
projection 

925 

60010  926 
* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for 
927 
singlestep rewriting with subterm selection based on patterns. 

928 

58630  929 

58066  930 
*** ML *** 
931 

60010  932 
* Subtle change of name space policy: undeclared entries are now 
933 
considered inaccessible, instead of accessible via the fullyqualified 

934 
internal name. This mainly affects Name_Space.intern (and derivatives), 

935 
which may produce an unexpected Long_Name.hidden prefix. Note that 

60011  936 
contemporary applications use the strict Name_Space.check (and 
60010  937 
derivatives) instead, which is not affected by the change. Potential 
938 
INCOMPATIBILITY in rare applications of Name_Space.intern. 

59951  939 

60096  940 
* Subtle change of error semantics of Toplevel.proof_of: regular user 
941 
ERROR instead of internal Toplevel.UNDEF. 

942 

59951  943 
* Basic combinators map, fold, fold_map, split_list, apply are available 
944 
as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. 

945 

946 
* Renamed "pairself" to "apply2", in accordance to @{apply 2}. 

947 
INCOMPATIBILITY. 

948 

949 
* Former combinators NAMED_CRITICAL and CRITICAL for central critical 

950 
sections have been discontinued, in favour of the more elementary 

951 
Multithreading.synchronized and its highlevel derivative 

952 
Synchronized.var (which is usually sufficient in applications). Subtle 

953 
INCOMPATIBILITY: synchronized access needs to be atomic and cannot be 

954 
nested. 

955 

60010  956 
* Synchronized.value (ML) is actually synchronized (as in Scala): subtle 
957 
change of semantics with minimal potential for INCOMPATIBILITY. 

59899  958 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

959 
* The main operations to certify logical entities are Thm.ctyp_of and 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

960 
Thm.cterm_of with a local context; oldstyle global theory variants are 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

961 
available as Thm.global_ctyp_of and Thm.global_cterm_of. 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

962 
INCOMPATIBILITY. 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

963 

59582  964 
* Elementary operations in module Thm are no longer pervasive. 
965 
INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, 

966 
Thm.term_of etc. 

967 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

968 
* Proper context for various elementary tactics: assume_tac, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59480
diff
changeset

969 
resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac, 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59480
diff
changeset

970 
compose_tac, Splitter.split_tac etc. INCOMPATIBILITY. 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58928
diff
changeset

971 

58066  972 
* Tactical PARALLEL_ALLGOALS is the most common way to refer to 
973 
PARALLEL_GOALS. 

974 

59564
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset

975 
* Goal.prove_multi is superseded by the fully general Goal.prove_common, 
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset

976 
which also allows to specify a fork priority. 
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset

977 

59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

978 
* Antiquotation @{command_spec "COMMAND"} is superseded by 
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

979 
@{command_keyword COMMAND} (usually without quotes and with PIDE 
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

980 
markup). Minor INCOMPATIBILITY. 
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

981 

60010  982 
* Cartouches within ML sources are turned into values of type 
983 
Input.source (with formal position information). 

984 

58066  985 

58610  986 
*** System *** 
987 

59951  988 
* The Isabelle tool "update_cartouches" changes theory files to use 
989 
cartouches instead of oldstyle {* verbatim *} or `alt_string` tokens. 

990 

60108  991 
* The Isabelle tool "build" provides new options X, k, x. 
59951  992 

993 
* Discontinued oldfashioned "codegen" tool. Code generation can always 

994 
be externally triggered using an appropriate ROOT file plus a 

995 
corresponding theory. Parametrization is possible using environment 

996 
variables, or ML snippets in the most extreme cases. Minor 

997 
INCOMPATIBILITY. 

58842  998 

59200  999 
* JVM system property "isabelle.threads" determines size of Scala thread 
1000 
pool, like Isabelle system option "threads" for ML. 

1001 

59201
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

1002 
* JVM system property "isabelle.laf" determines the default Swing 
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

1003 
lookandfeel, via internal class name or symbolic name as in the jEdit 
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

1004 
menu Global Options / Appearance. 
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

1005 

59951  1006 
* Support for Proof General and Isar TTY loop has been discontinued. 
60010  1007 
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead. 
59891
9ce697050455
added isabelle build option k, for fast offline checking of theory sources;
wenzelm
parents:
59849
diff
changeset

1008 

58610  1009 

57695  1010 

57452  1011 
New in Isabelle2014 (August 2014) 
1012 
 

54055  1013 

54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

1014 
*** General *** 
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

1015 

57452  1016 
* Support for official Standard ML within the Isabelle context. 
1017 
Command 'SML_file' reads and evaluates the given Standard ML file. 

1018 
Toplevel bindings are stored within the theory context; the initial 

1019 
environment is restricted to the Standard ML implementation of 

1020 
Poly/ML, without the addons of Isabelle/ML. Commands 'SML_import' 

1021 
and 'SML_export' allow to exchange toplevel bindings between the two 

1022 
separate environments. See also ~~/src/Tools/SML/Examples.thy for 

1023 
some examples. 

56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56450
diff
changeset

1024 

57504  1025 
* Standard tactics and proof methods such as "clarsimp", "auto" and 
1026 
"safe" now preserve equality hypotheses "x = expr" where x is a free 

1027 
variable. Locale assumptions and chained facts containing "x" 

1028 
continue to be useful. The new method "hypsubst_thin" and the 

1029 
configuration option "hypsubst_thin" (within the attribute name space) 

1030 
restore the previous behavior. INCOMPATIBILITY, especially where 

1031 
induction is done after these methods or when the names of free and 

1032 
bound variables clash. As first approximation, old proofs may be 

1033 
repaired by "using [[hypsubst_thin = true]]" in the critical spot. 

1034 

56232  1035 
* More static checking of proof methods, which allows the system to 
1036 
form a closure over the concrete syntax. Method arguments should be 

1037 
processed in the original proof context as far as possible, before 

1038 
operating on the goal state. In any case, the standard discipline for 

1039 
subgoaladdressing needs to be observed: no subgoals or a subgoal 

1040 
number that is out of range produces an empty result sequence, not an 

1041 
exception. Potential INCOMPATIBILITY for nonconformant tactical 

1042 
proof tools. 

1043 

57452  1044 
* Lexical syntax (inner and outer) supports text cartouches with 
1045 
arbitrary nesting, and without escapes of quotes etc. The Prover IDE 

1046 
supports input via ` (backquote). 

1047 

1048 
* The outer syntax categories "text" (for formal comments and document 

1049 
markup commands) and "altstring" (for literal fact references) allow 

1050 
cartouches as well, in addition to the traditional mix of quotations. 

1051 

1052 
* Syntax of document antiquotation @{rail} now uses \<newline> instead 

1053 
of "\\", to avoid the optical illusion of escaped backslash within 

57491  1054 
string token. General renovation of its syntax using text cartouches. 
57452  1055 
Minor INCOMPATIBILITY. 
1056 

1057 
* Discontinued legacy_isub_isup, which was a temporary workaround for 

1058 
Isabelle/ML in Isabelle20131. The prover process no longer accepts 

1059 
old identifier syntax with \<^isub> or \<^isup>. Potential 

1060 
INCOMPATIBILITY. 

1061 

1062 
* Document antiquotation @{url} produces markup for the given URL, 

1063 
which results in an active hyperlink within the text. 

1064 

1065 
* Document antiquotation @{file_unchecked} is like @{file}, but does 

1066 
not check existence within the filesystem. 

1067 

1068 
* Updated and extended manuals: codegen, datatypes, implementation, 

1069 
isarref, jedit, system. 

57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1070 

54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

1071 

54533  1072 
*** Prover IDE  Isabelle/Scala/jEdit *** 
1073 

57650  1074 
* Improved Document panel: simplified interaction where every single 
57452  1075 
mouse click (re)opens document via desktop environment or as jEdit 
1076 
buffer. 

1077 

1078 
* Support for Navigator plugin (with toolbar buttons), with connection 

1079 
to PIDE hyperlinks. 

1080 

1081 
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. 

1082 
Open text buffers take precedence over copies within the filesystem. 

1083 

1084 
* Improved support for Isabelle/ML, with jEdit mode "isabelleml" for 

1085 
auxiliary ML files. 

57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1086 

96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1087 
* Improved syntactic and semantic completion mechanism, with simple 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1088 
templates, completion language context, namespace completion, 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1089 
filename completion, spellchecker completion. 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1090 

96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1091 
* Refined GUI popup for completion: more robust key/mouse event 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1092 
handling and propagation to enclosing text area  avoid loosing 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1093 
keystrokes with slow / remote graphics displays. 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1094 

57833
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset

1095 
* Completion popup supports both ENTER and TAB (default) to select an 
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset

1096 
item, depending on Isabelle options. 
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset

1097 

57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1098 
* Refined insertion of completion items wrt. jEdit text: multiple 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1099 
selections, rectangular selections, rectangular selection as "tall 
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1100 
caret". 
56342  1101 

56580  1102 
* Integrated spellchecker for document text, comments etc. with 
57423
96f970d1522b
updated NEWS  removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset

1103 
completion popup and contextmenu. 
56554  1104 

56879
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset

1105 
* More general "Query" panel supersedes "Find" panel, with GUI access 
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset

1106 
to commands 'find_theorems' and 'find_consts', as well as print 
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset

1107 
operations for the context. Minor incompatibility in keyboard 
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset

1108 
shortcuts etc.: replace action isabellefind by isabellequery. 
56761  1109 

56901  1110 
* Search field for all output panels ("Output", "Query", "Info" etc.) 
1111 
to highlight text via regular expression. 

1112 

54881  1113 
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle / 
1114 
General") allows to specify additional print modes for the prover 

1115 
process, without requiring oldfashioned commandline invocation of 

1116 
"isabelle jedit m MODE". 

1117 

56505  1118 
* More support for remote files (e.g. http) using standard Java 
1119 
networking operations instead of jEdit virtual filesystems. 

1120 

57822  1121 
* Empty editors buffers that are no longer required (e.g.\ via theory 
1122 
imports) are automatically removed from the document model. 

1123 

57869  1124 
* Improved monitor panel. 
1125 

56838  1126 
* Improved Console/Scala plugin: more uniform scala.Console output, 
1127 
more robust treatment of threads and interrupts. 

1128 

56939  1129 
* Improved management of dockable windows: clarified keyboard focus 
1130 
and window placement wrt. main editor view; optional menu item to 

1131 
"Detach" a copy where this makes sense. 

1132 

57452  1133 
* New Simplifier Trace panel provides an interactive view of the 
57594
8c095aef6769
clarified "simp_trace_new" and corresponding isarref section;
wenzelm
parents:
57532
diff
changeset

1134 
simplification process, enabled by the "simp_trace_new" attribute 
57452  1135 
within the context. 
1136 

1137 

55001  1138 
*** Pure *** 
1139 

57504  1140 
* Lowlevel typeclass commands 'classes', 'classrel', 'arities' have 
1141 
been discontinued to avoid the danger of nontrivial axiomatization 

1142 
that is not immediately visible. INCOMPATIBILITY, use regular 

1143 
'instance' command with proof. The required OFCLASS(...) theorem 

1144 
might be postulated via 'axiomatization' beforehand, or the proof 

1145 
finished trivially if the underlying class definition is made vacuous 

1146 
(without any assumptions). See also Isabelle/ML operations 

1147 
Axclass.class_axiomatization, Axclass.classrel_axiomatization, 

1148 
Axclass.arity_axiomatization. 

1149 

56245  1150 
* Basic constants of Pure use more conventional names and are always 
1151 
qualified. Rare INCOMPATIBILITY, but with potentially serious 

1152 
consequences, notably for tools in Isabelle/ML. The following 

1153 
renaming needs to be applied: 

1154 

1155 
== ~> Pure.eq 

1156 
==> ~> Pure.imp 

1157 
all ~> Pure.all 

1158 
TYPE ~> Pure.type 

1159 
dummy_pattern ~> Pure.dummy_pattern 

1160 

1161 
Systematic porting works by using the following theory setup on a 

1162 
*previous* Isabelle version to introduce the new name accesses for the 

1163 
old constants: 

1164 

1165 
setup {* 

1166 
fn thy => thy 

1167 
> Sign.root_path 

1168 
> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "==" 

1169 
> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>" 

1170 
> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all" 

1171 
> Sign.restore_naming thy 

1172 
*} 

1173 

1174 
Thus ML antiquotations like @{const_name Pure.eq} may be used already. 

1175 
Later the application is moved to the current Isabelle version, and 

1176 
the auxiliary aliases are deleted. 

1177 

55143
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

1178 
* Attributes "where" and "of" allow an optional context of local 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

1179 
variables ('for' declaration): these variables become schematic in the 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

1180 
instantiated theorem. 
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset

1181 

55152  1182 
* Obsolete attribute "standard" has been discontinued (legacy since 
1183 
Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context 

1184 
where instantiations with schematic variables are intended (for 

1185 
declaration commands like 'lemmas' or attributes like "of"). The 

1186 
following temporary definition may help to port old applications: 

1187 

1188 
attribute_setup standard = 

1189 
"Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))" 

1190 

55001  1191 
* More thorough check of proof context for goal statements and 
55006  1192 
attributed fact expressions (concerning background theory, declared 
1193 
hyps). Potential INCOMPATIBILITY, tools need to observe standard 

1194 
context discipline. See also Assumption.add_assumes and the more 

1195 
primitive Thm.assume_hyps. 

55001  1196 

55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset

1197 
* Inner syntax token language allows regular quoted strings "..." 
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset

1198 
(only makes sense in practice, if outer syntax is delimited 
57452  1199 
differently, e.g. via cartouches). 
1200 

57504  1201 
* Command 'print_term_bindings' supersedes 'print_binds' for clarity, 
1202 
but the latter is retained some time as Proof General legacy. 

1203 

57452  1204 
* Code generator preprocessor: explicit control of simp tracing on a 
1205 
perconstant basis. See attribute "code_preproc". 

57430
020cea57eaa4
tracing facilities for the code generator preprocessor
haftmann
parents:
57423
diff
changeset

1206 

55001  1207 

54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset

1208 
*** HOL *** 
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset

1209 

57504  1210 
* Code generator: enforce case of identifiers only for strict target 
1211 
language requirements. INCOMPATIBILITY. 

1212 

1213 
* Code generator: explicit proof contexts in many ML interfaces. 

1214 
INCOMPATIBILITY. 

1215 

1216 
* Code generator: minimize exported identifiers by default. Minor 

1217 
INCOMPATIBILITY. 

1218 

1219 
* Code generation for SML and OCaml: dropped arcane "no_signatures" 

1220 
option. Minor INCOMPATIBILITY. 

1221 

1222 
* "declare [[code abort: ...]]" replaces "code_abort ...". 

1223 
INCOMPATIBILITY. 

1224 

1225 
* "declare [[code drop: ...]]" drops all code equations associated 

1226 
with the given constants. 

1227 

1228 
* Code generations are provided for make, fields, extend and truncate 

1229 
operations on records. 

57437  1230 

57452  1231 
* Command and antiquotation "value" are now hardcoded against nbe and 
1232 
ML. Minor INCOMPATIBILITY. 

1233 

57504  1234 
* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY. 
1235 

1236 
* The symbol "\<newline>" may be used within char or string literals 

1237 
to represent (Char Nibble0 NibbleA), i.e. ASCII newline. 

1238 

1239 
* Qualified String.implode and String.explode. INCOMPATIBILITY. 

56923  1240 

57452  1241 
* Simplifier: Enhanced solver of preconditions of rewrite rules can 
1242 
now deal with conjunctions. For help with converting proofs, the old 

1243 
behaviour of the simplifier can be restored like this: declare/using 

1244 
[[simp_legacy_precond]]. This configuration option will disappear 

1245 
again in the future. INCOMPATIBILITY. 

56073
29e308b56d23
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents:
56072
diff
changeset

1246 

55139  1247 
* Simproc "finite_Collect" is no longer enabled by default, due to 
1248 
spurious crashes and other surprises. Potential INCOMPATIBILITY. 

1249 

57452  1250 
* Moved new (co)datatype package and its dependencies from session 
1251 
"HOLBNF" to "HOL". The commands 'bnf', 'wrap_free_constructors', 

1252 
'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now 

1253 
part of theory "Main". 

1254 

55098  1255 
Theory renamings: 
1256 
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) 

1257 
Library/Wfrec.thy ~> Wfrec.thy 

1258 
Library/Zorn.thy ~> Zorn.thy 

1259 
Cardinals/Order_Relation.thy ~> Order_Relation.thy 

1260 
Library/Order_Union.thy ~> Cardinals/Order_Union.thy 

1261 
Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy 

1262 
Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy 

1263 
Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy 

1264 
Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy 

1265 
Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy 

1266 
BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy 

1267 
BNF/Basic_BNFs.thy ~> Basic_BNFs.thy 

1268 
BNF/BNF_Comp.thy ~> BNF_Comp.thy 

1269 
BNF/BNF_Def.thy ~> BNF_Def.thy 

1270 
BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy 

1271 
BNF/BNF_GFP.thy ~> BNF_GFP.thy 

1272 
BNF/BNF_LFP.thy ~> BNF_LFP.thy 

1273 
BNF/BNF_Util.thy ~> BNF_Util.thy 

1274 
BNF/Coinduction.thy ~> Coinduction.thy 

1275 
BNF/More_BNFs.thy ~> Library/More_BNFs.thy 

1276 
BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy 

1277 
BNF/Examples/* ~> BNF_Examples/* 

57452  1278 

55098  1279 
New theories: 
1280 
Wellorder_Extension.thy (split from Zorn.thy) 

1281 
Library/Cardinal_Notations.thy 

56942  1282 
Library/BNF_Axomatization.thy 
55098  1283 
BNF_Examples/Misc_Primcorec.thy 
1284 
BNF_Examples/Stream_Processor.thy 

57452  1285 

55519  1286 
Discontinued theories: 
55098  1287 
BNF/BNF.thy 
1288 
BNF/Equiv_Relations_More.thy 

57452  1289 

1290 
INCOMPATIBILITY. 

55098  1291 

56118
d3967fdc800a
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
blanchet
parents:
56076
diff
changeset

1292 
* New (co)datatype package: 
57452  1293 
 Command 'primcorec' is fully implemented. 
1294 
 Command 'datatype_new' generates size functions ("size_xxx" and 

1295 
"size") as required by 'fun'. 

1296 
 BNFs are integrated with the Lifting tool and newstyle 

1297 
(co)datatypes with Transfer. 

1298 
 Renamed commands: 

55875  1299 
datatype_new_compat ~> datatype_compat 
1300 
primrec_new ~> primrec 

1301 
wrap_free_constructors ~> free_constructors 

1302 
INCOMPATIBILITY. 

57452  1303 
 The generated constants "xxx_case" and "xxx_rec" have been renamed 
55875  1304 
"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod"). 
1305 
INCOMPATIBILITY. 

57452  1306 
 The constant "xxx_(un)fold" and related theorems are no longer 
1307 
generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually 

1308 
using "prim(co)rec". 

55875  1309 
INCOMPATIBILITY. 
57452  1310 
 No discriminators are generated for nullary constructors by 
1311 
default, eliminating the need for the odd "=:" syntax. 

57091  1312 
INCOMPATIBILITY. 
57452  1313 
 No discriminators or selectors are generated by default by 
57094
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

1314 
"datatype_new", unless custom names are specified or the new 
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

1315 
"discs_sels" option is passed. 
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset

1316 
INCOMPATIBILITY. 
55875  1317 

55643  1318 
* Old datatype package: 
57452  1319 
 The generated theorems "xxx.cases" and "xxx.recs" have been 
1320 
renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" > 

1321 
"sum.case"). INCOMPATIBILITY. 

1322 
 The generated constants "xxx_case", "xxx_rec", and "xxx_size" have 

1323 
been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., 

1324 
"prod_case" ~> "case_prod"). INCOMPATIBILITY. 

1325 

1326 
* The types "'a list" and "'a option", their set and map functions, 

1327 
their relators, and their selectors are now produced using the new 

1328 
BNFbased datatype package. 

1329 

55519  1330 
Renamed constants: 
1331 
Option.set ~> set_option 

1332 
Option.map ~> map_option 

55525  1333 
option_rel ~> rel_option 
57452  1334 

55519  1335 
Renamed theorems: 
55585  1336 
set_def ~> set_rec[abs_def] 
55519  1337 
map_def ~> map_rec[abs_def] 
1338 
Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") 

56652  1339 
option.recs ~> option.rec 
55524
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55519
diff
changeset

1340 
list_all2_def ~> list_all2_iff 
55585  1341 
set.simps ~> set_simps (or the slightly different "list.set") 
55519  1342 
map.simps ~> list.map 
1343 
hd.simps ~> list.sel(1) 

1344 
tl.simps ~> list.sel(23) 

1345 
the.simps ~> option.sel 

57452  1346 

1347 
INCOMPATIBILITY. 

55519  1348 

55933  1349 
* The following map functions and relators have been renamed: 
55939  1350 
sum_map ~> map_sum 
1351 
map_pair ~> map_prod 

55944  1352 
prod_rel ~> rel_prod 
55943  1353 
sum_rel ~> rel_sum 
55945  1354 
fun_rel ~> rel_fun 
55942  1355 
set_rel ~> rel_set 
1356 
filter_rel ~> rel_filter 

57452  1357 
fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy") 
1358 
cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy") 

1359 
vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy") 

1360 

1361 
INCOMPATIBILITY. 

1362 

57826  1363 
* Lifting and Transfer: 
1364 
 a type variable as a raw type is supported 

1365 
 stronger reflexivity prover 

1366 
 rep_eq is always generated by lift_definition 

57856  1367 
 setup for Lifting/Transfer is now automated for BNFs 
57826  1368 
+ holds for BNFs that do not contain a dead variable 
57856  1369 
+ relator_eq, relator_mono, relator_distr, relator_domain, 
57826  1370 
relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total, 
1371 
right_unique, right_total, left_unique, left_total are proved 

1372 
automatically 

1373 
+ definition of a predicator is generated automatically 

1374 
+ simplification rules for a predicator definition are proved 

1375 
automatically for datatypes 

1376 
 consolidation of the setup of Lifting/Transfer 

57856  1377 
+ property that a relator preservers reflexivity is not needed any 
57826  1378 
more 
1379 
Minor INCOMPATIBILITY. 

57856  1380 
+ left_total and left_unique rules are now transfer rules 
57826  1381 
(reflexivity_rule attribute not needed anymore) 
1382 
INCOMPATIBILITY. 

57856  1383 
+ Domainp does not have to be a separate assumption in 
57826  1384 
relator_domain theorems (=> more natural statement) 
1385 
INCOMPATIBILITY. 

1386 
 registration of code equations is more robust 

1387 
Potential INCOMPATIBILITY. 

1388 
 respectfulness proof obligation is preprocessed to a more readable 

1389 
form 

1390 
Potential INCOMPATIBILITY. 

1391 
 eq_onp is always unfolded in respectfulness proof obligation 

1392 
Potential INCOMPATIBILITY. 

57856  1393 
 unregister lifting setup for Code_Numeral.integer and 
57826  1394 
Code_Numeral.natural 
1395 
Potential INCOMPATIBILITY. 

1396 
 Lifting.invariant > eq_onp 

1397 
INCOMPATIBILITY. 

57856  1398 

57508  1399 
* New internal SAT solver "cdclite" that produces models and proof 
1400 
traces. This solver replaces the internal SAT solvers "enumerate" and 

1401 
"dpll". Applications that explicitly used one of these two SAT 
