author  kleing 
Sun, 18 May 2003 15:28:41 +0200  
changeset 14035  c46ce87960fb 
parent 14018  3ef6c509f29c 
child 14119  fb9c392644a1 
permissions  rwrr 
5363  1 
Isabelle NEWS  history userrelevant changes 
2 
============================================== 

2553  3 

13280
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

4 
New in this Isabelle release 
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

5 
 
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

6 

306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

7 
*** General *** 
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

8 

13618  9 
* Provers/simplifier: 
10 

13781  11 
 Completely reimplemented method simp (ML: Asm_full_simp_tac): 
13618  12 
Assumptions are now subject to complete mutual simplification, 
13 
not just from left to right. The simplifier now preserves 

14 
the order of assumptions. 

15 

16 
Potential INCOMPATIBILITY: 

17 

13781  18 
 simp sometimes diverges where the old version did 
19 
not, e.g. invoking simp on the goal 

13618  20 

21 
[ P (f x); y = x; f x = f y ] ==> Q 

22 

13781  23 
now gives rise to the infinite reduction sequence 
24 

25 
P(f x) (f x = f y)> P(f y) (y = x)> P(f x) (f x = f y)> ... 

26 

27 
Using "simp (asm_lr)" (ML: Asm_lr_simp_tac) instead often solves this 

28 
kind of problem. 

29 

30 
 Tactics combining classical reasoner and simplification (such as auto) 

31 
are also affected by this change, because many of them rely on 

32 
simp. They may sometimes diverge as well or yield a different numbers 

33 
of subgoals. Try to use e.g. force, fastsimp, or safe instead of auto 

34 
in case of problems. Sometimes subsequent calls to the classical 

35 
reasoner will fail because a preceeding call to the simplifier too 

36 
eagerly simplified the goal, e.g. deleted redundant premises. 

13618  37 

38 
 The simplifier trace now shows the names of the applied rewrite rules 

39 

13829  40 
 You can limit the number of recursive invocations of the simplifier 
41 
during conditional rewriting (where the simplifie tries to solve the 

42 
conditions before applying the rewrite rule): 

43 
ML "simp_depth_limit := n" 

44 
where n is an integer. Thus you can force termination where previously 

45 
the simplifier would diverge. 

46 

13835
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13829
diff
changeset

47 
 Accepts free variables as head terms in congruence rules. Useful in Isar. 
13829  48 

13938  49 
 No longer aborts on failed congruence proof. Instead, the 
50 
congruence is ignored. 

51 

14008  52 
* Pure: New generic framework for extracting programs from constructive 
53 
proofs. See HOL/Extraction.thy for an example instantiation, as well 

54 
as HOL/Extraction for some case studies. 

55 

13868  56 
* Pure: The main goal of the proof state is no longer shown by default, only 
57 
the subgoals. This behaviour is controlled by a new flag. 

13835
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13829
diff
changeset

58 
PG menu: Isabelle/Isar > Settings > Show Main Goal 
13815  59 
(ML: Proof.show_main_goal). 
60 

61 
* Pure: You can find all matching introduction rules for subgoal 1, i.e. all 

62 
rules whose conclusion matches subgoal 1: 

63 
PG menu: Isabelle/Isar > Show me > matching rules 

64 
The rules are ordered by how closely they match the subgoal. 

65 
In particular, rules that solve a subgoal outright are displayed first 

66 
(or rather last, the way they are printed). 

67 
(ML: ProofGeneral.print_intros()) 

68 

69 
* Pure: New flag trace_unify_fail causes unification to print 

13781  70 
diagnostic information (PG: in trace buffer) when it fails. This is 
71 
useful for figuring out why single step proofs like rule, erule or 

72 
assumption failed. 

73 

13815  74 
* Pure: Locale specifications now produce predicate definitions 
13410
f2cd09766864
* Pure: locale specifications now produce predicate definitions;
wenzelm
parents:
13344
diff
changeset

75 
according to the body of text (covering assumptions modulo local 
f2cd09766864
* Pure: locale specifications now produce predicate definitions;
wenzelm
parents:
13344
diff
changeset

76 
definitions); predicate "loc_axioms" covers newly introduced text, 
f2cd09766864
* Pure: locale specifications now produce predicate definitions;
wenzelm
parents:
13344
diff
changeset

77 
while "loc" is cumulative wrt. all included locale expressions; the 
f2cd09766864
* Pure: locale specifications now produce predicate definitions;
wenzelm
parents:
13344
diff
changeset

78 
latter view is presented only on export into the global theory 
f2cd09766864
* Pure: locale specifications now produce predicate definitions;
wenzelm
parents:
13344
diff
changeset

79 
context; potential INCOMPATIBILITY, use "(open)" option to fall back 
f2cd09766864
* Pure: locale specifications now produce predicate definitions;
wenzelm
parents:
13344
diff
changeset

80 
on the old view without predicates; 
f2cd09766864
* Pure: locale specifications now produce predicate definitions;
wenzelm
parents:
13344
diff
changeset

81 

13459
83f41b047a39
* Pure: predefined locales "var" and "struct" are useful for sharing
wenzelm
parents:
13443
diff
changeset

82 
* Pure: predefined locales "var" and "struct" are useful for sharing 
83f41b047a39
* Pure: predefined locales "var" and "struct" are useful for sharing
wenzelm
parents:
13443
diff
changeset

83 
parameters (as in CASL, for example); just specify something like 
83f41b047a39
* Pure: predefined locales "var" and "struct" are useful for sharing
wenzelm
parents:
13443
diff
changeset

84 
``var x + var y + struct M'' as import; 
83f41b047a39
* Pure: predefined locales "var" and "struct" are useful for sharing
wenzelm
parents:
13443
diff
changeset

85 

13463
07747943c626
* Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm
parents:
13459
diff
changeset

86 
* Pure: improved thms_containing: proper indexing of facts instead of 
07747943c626
* Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm
parents:
13459
diff
changeset

87 
raw theorems; check validity of results wrt. current name space; 
07747943c626
* Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm
parents:
13459
diff
changeset

88 
include local facts of proof configuration (also covers active 
13541  89 
locales), cover fixed variables in index; may use "_" in term 
90 
specification; an optional limit for the number of printed facts may 

91 
be given (the default is 40); 

92 

93 
* Pure: disallow duplicate fact bindings within newstyle theory files 

94 
(batchmode only); 

13540
aede0306e214
* Pure: disallow duplicate fact bindings within newstyle theory files;
wenzelm
parents:
13522
diff
changeset

95 

13463
07747943c626
* Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm
parents:
13459
diff
changeset

96 
* Provers: improved induct method: assumptions introduced by case 
07747943c626
* Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm
parents:
13459
diff
changeset

97 
"foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from 
07747943c626
* Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm
parents:
13459
diff
changeset

98 
the goal statement); "foo" still refers to all facts collectively; 
07747943c626
* Provers: Simplifier.simproc(_i) now provide sane interface for
wenzelm
parents:
13459
diff
changeset

99 

13550  100 
* Provers: the function blast.overloaded has been removed: all constants 
101 
are regarded as potentially overloaded, which improves robustness in exchange 

102 
for slight decrease in efficiency; 

103 

13781  104 
* Provers/linorder: New generic prover for transitivity reasoning over 
105 
linear orders. Note: this prover is not efficient! 

106 

13522
934fffeb6f38
* Isar: preview of problems to finish 'show' now produce an error
wenzelm
parents:
13518
diff
changeset

107 
* Isar: preview of problems to finish 'show' now produce an error 
934fffeb6f38
* Isar: preview of problems to finish 'show' now produce an error
wenzelm
parents:
13518
diff
changeset

108 
rather than just a warning (in interactive mode); 
934fffeb6f38
* Isar: preview of problems to finish 'show' now produce an error
wenzelm
parents:
13518
diff
changeset

109 

13280
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

110 

13158  111 
*** HOL *** 
112 

13899  113 
* arith(_tac) 
114 

115 
 Produces a counter example if it cannot prove a goal. 

116 
Note that the counter example may be spurious if the goal is not a formula 

117 
of quantifierfree linear arithmetic. 

118 
In ProofGeneral the counter example appears in the trace buffer. 

119 

120 
 Knows about div k and mod k where k is a numeral of type nat or int. 

121 

122 
 Calls full Presburger arithmetic (by Amine Chaieb) if quantifierfree 

123 
linear arithmetic fails. This takes account of quantifiers and divisibility. 

124 
Presburger arithmetic can also be called explicitly via presburger(_tac). 

125 

126 
* simp's arithmetic capabilities have been enhanced a bit: it now 

127 
takes ~= in premises into account (by performing a case split); 

128 

129 
* simp reduces "m*(n div m) + n mod m" to n, even if the two summands 

130 
are distributed over a sum of terms; 

131 

13735  132 
* New tactic "trans_tac" and method "trans" instantiate 
133 
Provers/linorder.ML for axclasses "order" and "linorder" (predicates 

134 
"<=", "<" and "="). 

135 

13587  136 
* function INCOMPATIBILITIES: Pisets have been redefined and moved from main 
137 
HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp"; 

138 

13443  139 
* 'typedef' command has new option "open" to suppress the set 
140 
definition; 

141 

13522
934fffeb6f38
* Isar: preview of problems to finish 'show' now produce an error
wenzelm
parents:
13518
diff
changeset

142 
* functions Min and Max on finite sets have been introduced (theory 
934fffeb6f38
* Isar: preview of problems to finish 'show' now produce an error
wenzelm
parents:
13518
diff
changeset

143 
Finite_Set); 
13492  144 

13443  145 
* attribute [symmetric] now works for relations as well; it turns 
146 
(x,y) : R^1 into (y,x) : R, and vice versa; 

147 

13613  148 
* induct over a !!quantified statement (say !!x1..xn): 
149 
each "case" automatically performs "fix x1 .. xn" with exactly those names. 

150 

13899  151 
* Map: `empty' is no longer a constant but a syntactic abbreviation for 
152 
%x. None. Warning: empty_def now refers to the previously hidden definition 

153 
of the empty set. 

154 

14018  155 
* Algebra: formalization of classical algebra. Intended as base for 
156 
any algebraic development in Isabelle. Currently covers group theory 

157 
(up to Sylow's theorem) and ring theory (Universal Property of 

158 
Univariate Polynomials). Contributions welcome; 

13960  159 

160 
* GroupTheory: deleted, since its material has been moved to Algebra; 

161 

13966
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

162 
* Complex: new directory of the complex numbers with numeric constants, 
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

163 
nonstandard complex numbers, and some complex analysis, standard and 
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

164 
nonstandard (Jacques Fleuriot); 
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

165 

2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

166 
* HOLComplex: new image for analysis, replacing HOLReal and HOLHyperreal; 
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

167 

2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

168 
* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques 
2160abf7cfe7
removal of the image HOLReal and merging of HOLRealex with HOLComplexex
paulson
parents:
13960
diff
changeset

169 
Fleuriot); 
13960  170 

13549  171 
* Real/HahnBanach: updated and adapted to locales; 
172 

13995  173 
* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, 
174 
Gray and Kramer); 

13872  175 

176 
* UNITY: added the MeierSanders theory of progress sets; 

177 

14011  178 
* MicroJava: bytecode verifier and lightweight bytecode verifier 
179 
as abstract algorithms, instantiated to the JVM; 

180 

14010  181 
* Bali: Java source language formalization. Type system, operational 
182 
semantics, axiomatic semantics. Supported language features: 

183 
classes, interfaces, objects,virtual methods, static methods, 

184 
static/instance fields, arrays, access modifiers, definite 

185 
assignment, exceptions. 

13549  186 

14011  187 

13549  188 
*** ZF *** 
189 

190 
* ZF/Constructible: consistency proof for AC (Gödel's constructible 

191 
universe, etc.); 

192 

13872  193 
* Main ZF: virtually all theories converted to newstyle format; 
13518  194 

13280
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

195 

13478  196 
*** ML *** 
197 

198 
* Pure: Tactic.prove provides sane interface for internal proofs; 

199 
omits the infamous "standard" operation, so this is more appropriate 

200 
than prove_goalw_cterm in many situations (e.g. in simprocs); 

201 

202 
* Pure: improved error reporting of simprocs; 

203 

204 
* Provers: Simplifier.simproc(_i) provides sane interface for setting 

205 
up simprocs; 

206 

207 

13953  208 
*** Document preparation *** 
209 

210 
* uses \par instead of \\ for line breaks in theory text. This may 

211 
shift some page breaks in large documents. To get the old behaviour 

212 
use \renewcommand{\isanewline}{\mbox{}\\\mbox{}} in root.tex. 

213 

214 
* minimized dependencies of isabelle.sty and isabellesym.sty on 

215 
other packages 

216 

217 
* \<euro> now needs package babel/greek instead of marvosym (which 

218 
broke \Rightarrow) 

219 

13954  220 
* normal size for \<zero>...\<nine> (uses \mathbf instead of 
221 
textcomp package) 

13953  222 

13280
306ef3aef61b
* improved thms_containing: proper indexing of facts instead of raw
wenzelm
parents:
13190
diff
changeset

223 

12984  224 
New in Isabelle2002 (March 2002) 
225 
 

11474  226 

11572  227 
*** Document preparation *** 
228 

11842
b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

229 
* greatly simplified document preparation setup, including more 
b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

230 
graceful interpretation of isatool usedir i/d/D options, and more 
b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

231 
instructive isatool mkdir; users should basically be able to get 
12899
7d5b690253ee
"isatool usedir D output HOL Test && isatool document Test/output";
wenzelm
parents:
12889
diff
changeset

232 
started with "isatool mkdir HOL Test && isatool make"; alternatively, 
7d5b690253ee
"isatool usedir D output HOL Test && isatool document Test/output";
wenzelm
parents:
12889
diff
changeset

233 
users may run a separate document processing stage manually like this: 
7d5b690253ee
"isatool usedir D output HOL Test && isatool document Test/output";
wenzelm
parents:
12889
diff
changeset

234 
"isatool usedir D output HOL Test && isatool document Test/output"; 
11842
b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

235 

b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

236 
* theory dependency graph may now be incorporated into documents; 
b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

237 
isatool usedir g true will produce session_graph.eps/.pdf for use 
b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

238 
with \includegraphics of LaTeX; 
b903d3dabbe2
* greatly simplified document preparation setup, including more
wenzelm
parents:
11817
diff
changeset

239 

11864
371ce685b0ec
* proper spacing of consecutive markup elements, especially text
wenzelm
parents:
11842
diff
changeset

240 
* proper spacing of consecutive markup elements, especially text 
371ce685b0ec
* proper spacing of consecutive markup elements, especially text
wenzelm
parents:
11842
diff
changeset

241 
blocks after section headings; 
371ce685b0ec
* proper spacing of consecutive markup elements, especially text
wenzelm
parents:
11842
diff
changeset

242 

11572  243 
* support bold style (for single symbols only), input syntax is like 
244 
this: "\<^bold>\<alpha>" or "\<^bold>A"; 

245 

11814  246 
* \<bullet> is now output as bold \cdot by default, which looks much 
11572  247 
better in printed text; 
248 

11712
deb8cac87063
* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
wenzelm
parents:
11702
diff
changeset

249 
* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; 
deb8cac87063
* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
wenzelm
parents:
11702
diff
changeset

250 
note that these symbols are currently unavailable in Proof General / 
12769  251 
XSymbol; new symbols \<zero>, \<one>, ..., \<nine>, and \<euro>; 
12690  252 

253 
* isatool latex no longer depends on changed TEXINPUTS, instead 

254 
isatool document copies the Isabelle style files to the target 

255 
location; 

11712
deb8cac87063
* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
wenzelm
parents:
11702
diff
changeset

256 

11572  257 

11633  258 
*** Isar *** 
259 

12312
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

260 
* Pure/Provers: improved proof by cases and induction; 
12280  261 
 'case' command admits impromptu naming of parameters (such as 
262 
"case (Suc n)"); 

263 
 'induct' method divinates rule instantiation from the inductive 

264 
claim; no longer requires excessive ?P bindings for proper 

265 
instantiation of cases; 

266 
 'induct' method properly enumerates all possibilities of set/type 

267 
rules; as a consequence facts may be also passed through *type* 

268 
rules without further ado; 

269 
 'induct' method now derives symbolic cases from the *rulified* 

270 
rule (before it used to rulify cases stemming from the internal 

271 
atomized version); this means that the context of a nonatomic 

272 
statement becomes is included in the hypothesis, avoiding the 

273 
slightly cumbersome show "PROP ?case" form; 

274 
 'induct' may now use elimstyle induction rules without chaining 

275 
facts, using ``missing'' premises from the goal state; this allows 

276 
rules stemming from inductive sets to be applied in unstructured 

277 
scripts, while still benefitting from proper handling of nonatomic 

278 
statements; NB: major inductive premises need to be put first, all 

279 
the rest of the goal is passed through the induction; 

280 
 'induct' proper support for mutual induction involving nonatomic 

281 
rule statements (uses the new concept of simultaneous goals, see 

282 
below); 

12853  283 
 append all possible rule selections, but only use the first 
284 
success (no backtracking); 

11995
4a622f5fb164
 'induct' may now use elimstyle induction rules without chaining
wenzelm
parents:
11986
diff
changeset

285 
 removed obsolete "(simplified)" and "(stripped)" options of methods; 
12754
044a59921f3b
Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
wenzelm
parents:
12753
diff
changeset

286 
 undeclared rule case names default to numbers 1, 2, 3, ...; 
044a59921f3b
Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
wenzelm
parents:
12753
diff
changeset

287 
 added 'print_induct_rules' (covered by help item in recent Proof 
044a59921f3b
Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
wenzelm
parents:
12753
diff
changeset

288 
General versions); 
11995
4a622f5fb164
 'induct' may now use elimstyle induction rules without chaining
wenzelm
parents:
11986
diff
changeset

289 
 moved induct/cases attributes to Pure, methods to Provers; 
4a622f5fb164
 'induct' may now use elimstyle induction rules without chaining
wenzelm
parents:
11986
diff
changeset

290 
 generic method setup instantiated for FOL and HOL; 
11986
26b95a6f3f79
 'induct' method now derives symbolic cases from the *rulified* rule
wenzelm
parents:
11965
diff
changeset

291 

12163
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

292 
* Pure: support multiple simultaneous goal statements, for example 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

293 
"have a: A and b: B" (same for 'theorem' etc.); being a pure 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

294 
metalevel mechanism, this acts as if several individual goals had 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

295 
been stated separately; in particular common proof methods need to be 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

296 
repeated in order to cover all claims; note that a single elimination 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

297 
step is *not* sufficient to establish the two conjunctions, so this 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

298 
fails: 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

299 

04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

300 
assume "A & B" then have A and B .. (*".." fails*) 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

301 

04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

302 
better use "obtain" in situations as above; alternative refer to 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

303 
multistep methods like 'auto', 'simp_all', 'blast+' etc.; 
04c98351f9af
Isar: 'induct' proper support for mutual induction involving
wenzelm
parents:
12159
diff
changeset

304 

12078
4eb8061286e5
* Isar/Pure: proper integration with ``locales''; unlike the original
wenzelm
parents:
12034
diff
changeset

305 
* Pure: proper integration with ``locales''; unlike the original 
12210
2f510d8d8291
* ZF: newstyle theory commands '(co)inductive', '(co)datatype',
wenzelm
parents:
12177
diff
changeset

306 
version by Florian Kammüller, Isar locales package highlevel proof 
12078
4eb8061286e5
* Isar/Pure: proper integration with ``locales''; unlike the original
wenzelm
parents:
12034
diff
changeset

307 
contexts rather than raw logical ones (e.g. we admit to include 
12280  308 
attributes everywhere); operations on locales include merge and 
12964  309 
rename; support for implicit arguments (``structures''); simultaneous 
310 
typeinference over imports and text; see also HOL/ex/Locales.thy for 

311 
some examples; 

12078
4eb8061286e5
* Isar/Pure: proper integration with ``locales''; unlike the original
wenzelm
parents:
12034
diff
changeset

312 

12707
4013be8572c5
* Pure: localized 'lemmas', 'theorems', 'declare';
wenzelm
parents:
12690
diff
changeset

313 
* Pure: the following commands have been ``localized'', supporting a 
4013be8572c5
* Pure: localized 'lemmas', 'theorems', 'declare';
wenzelm
parents:
12690
diff
changeset

314 
target locale specification "(in name)": 'lemma', 'theorem', 
4013be8572c5
* Pure: localized 'lemmas', 'theorems', 'declare';
wenzelm
parents:
12690
diff
changeset

315 
'corollary', 'lemmas', 'theorems', 'declare'; the results will be 
4013be8572c5
* Pure: localized 'lemmas', 'theorems', 'declare';
wenzelm
parents:
12690
diff
changeset

316 
stored both within the locale and at the theory level (exported and 
4013be8572c5
* Pure: localized 'lemmas', 'theorems', 'declare';
wenzelm
parents:
12690
diff
changeset

317 
qualified by the locale name); 
4013be8572c5
* Pure: localized 'lemmas', 'theorems', 'declare';
wenzelm
parents:
12690
diff
changeset

318 

12964  319 
* Pure: theory goals may now be specified in ``long'' form, with 
320 
adhoc contexts consisting of arbitrary locale elements. for example 

321 
``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and 

322 
definitions may be given, too); the result is a metalevel rule with 

323 
the context elements being discharged in the obvious way; 

324 

325 
* Pure: new proof command 'using' allows to augment currently used 

326 
facts after a goal statement ('using' is syntactically analogous to 

327 
'apply', but acts on the goal's facts only); this allows chained facts 

328 
to be separated into parts given before and after a claim, as in 

329 
``from a and b have C using d and e <proof>''; 

12078
4eb8061286e5
* Isar/Pure: proper integration with ``locales''; unlike the original
wenzelm
parents:
12034
diff
changeset

330 

11722  331 
* Pure: renamed "antecedent" case to "rule_context"; 
332 

12964  333 
* Pure: new 'judgment' command records explicit information about the 
334 
objectlogic embedding (used by several tools internally); no longer 

335 
use hardwired "Trueprop"; 

336 

11738  337 
* Pure: added 'corollary' command; 
338 

11722  339 
* Pure: fixed 'token_translation' command; 
340 

11899  341 
* Pure: removed obsolete 'exported' attribute; 
342 

11933  343 
* Pure: dummy pattern "_" in is/let is now automatically lifted over 
344 
bound variables: "ALL x. P x > Q x" (is "ALL x. _ > ?C x") 

11899  345 
supersedes more cumbersome ... (is "ALL x. _ x > ?C x"); 
346 

11952
b10f1e8862f4
* Pure: method 'atomize' presents local goal premises as objectlevel
wenzelm
parents:
11937
diff
changeset

347 
* Pure: method 'atomize' presents local goal premises as objectlevel 
b10f1e8862f4
* Pure: method 'atomize' presents local goal premises as objectlevel
wenzelm
parents:
11937
diff
changeset

348 
statements (atomic metalevel propositions); setup controlled via 
b10f1e8862f4
* Pure: method 'atomize' presents local goal premises as objectlevel
wenzelm
parents:
11937
diff
changeset

349 
rewrite rules declarations of 'atomize' attribute; example 
b10f1e8862f4
* Pure: method 'atomize' presents local goal premises as objectlevel
wenzelm
parents:
11937
diff
changeset

350 
application: 'induct' method with proper rule statements in improper 
b10f1e8862f4
* Pure: method 'atomize' presents local goal premises as objectlevel
wenzelm
parents:
11937
diff
changeset

351 
proof *scripts*; 
b10f1e8862f4
* Pure: method 'atomize' presents local goal premises as objectlevel
wenzelm
parents:
11937
diff
changeset

352 

12106
4a8558dbb6a0
* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,
wenzelm
parents:
12078
diff
changeset

353 
* Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.) 
4a8558dbb6a0
* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,
wenzelm
parents:
12078
diff
changeset

354 
now consider the syntactic context of assumptions, giving a better 
4a8558dbb6a0
* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,
wenzelm
parents:
12078
diff
changeset

355 
chance to get typeinference of the arguments right (this is 
4a8558dbb6a0
* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,
wenzelm
parents:
12078
diff
changeset

356 
especially important for locales); 
4a8558dbb6a0
* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,
wenzelm
parents:
12078
diff
changeset

357 

12312
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

358 
* Pure: "sorry" no longer requires quick_and_dirty in interactive 
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

359 
mode; 
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

360 

12405
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

361 
* Pure/obtain: the formal conclusion "thesis", being marked as 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

362 
``internal'', may no longer be reference directly in the text; 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

363 
potential INCOMPATIBILITY, may need to use "?thesis" in rare 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

364 
situations; 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

365 

9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

366 
* Pure: generic 'sym' attribute which declares a rule both as pure 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

367 
'elim?' and for the 'symmetric' operation; 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

368 

12877
b9635eb8a448
* Isar/Pure: marginal comments ``'' may now occur just anywhere in the text;
wenzelm
parents:
12853
diff
changeset

369 
* Pure: marginal comments ``'' may now occur just anywhere in the 
b9635eb8a448
* Isar/Pure: marginal comments ``'' may now occur just anywhere in the text;
wenzelm
parents:
12853
diff
changeset

370 
text; the fixed correlation with particular command syntax has been 
b9635eb8a448
* Isar/Pure: marginal comments ``'' may now occur just anywhere in the text;
wenzelm
parents:
12853
diff
changeset

371 
discontinued; 
b9635eb8a448
* Isar/Pure: marginal comments ``'' may now occur just anywhere in the text;
wenzelm
parents:
12853
diff
changeset

372 

13023
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

373 
* Pure: new method 'rules' is particularly wellsuited for proof 
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

374 
search in intuitionistic logic; a bit slower than 'blast' or 'fast', 
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

375 
but often produces more compact proof terms with less detours; 
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

376 

12364
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

377 
* Pure/Provers/classical: simplified integration with pure rule 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

378 
attributes and methods; the classical "intro?/elim?/dest?" 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

379 
declarations coincide with the pure ones; the "rule" method no longer 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

380 
includes classically swapped intros; "intro" and "elim" methods no 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

381 
longer pick rules from the context; also got rid of ML declarations 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

382 
AddXIs/AddXEs/AddXDs; all of this has some potential for 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

383 
INCOMPATIBILITY; 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

384 

12405
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

385 
* Provers/classical: attribute 'swapped' produces classical inversions 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

386 
of introduction rules; 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

387 

12364
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

388 
* Provers/simplifier: 'simplified' attribute may refer to explicit 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

389 
rules instead of full simplifier context; 'iff' attribute handles 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

390 
conditional rules; 
11936
fef099613354
* Provers: 'simplified' attribute may refer to explicit rules instead
wenzelm
parents:
11933
diff
changeset

391 

11745
06cd8c3b5487
* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
wenzelm
parents:
11738
diff
changeset

392 
* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms; 
06cd8c3b5487
* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
wenzelm
parents:
11738
diff
changeset

393 

11690  394 
* HOL: 'recdef' now fails on unfinished automated proofs, use 
11633  395 
"(permissive)" option to recover old behavior; 
396 

11933  397 
* HOL: 'inductive' no longer features separate (collective) attributes 
398 
for 'intros' (was found too confusing); 

399 

12405
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

400 
* HOL: properly declared induction rules less_induct and 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

401 
wf_induct_rule; 
9b16f99fd7b9
* Pure/obtain: "thesis" now internal (use ?thesis);
wenzelm
parents:
12364
diff
changeset

402 

11788
60054fee3c16
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
11745
diff
changeset

403 

11474  404 
*** HOL *** 
405 

11702  406 
* HOL: moved over to sane numeral syntax; the new policy is as 
407 
follows: 

408 

409 
 0 and 1 are polymorphic constants, which are defined on any 

410 
numeric type (nat, int, real etc.); 

411 

412 
 2, 3, 4, ... and 1, 2, 3, ... are polymorphic numerals, based 

413 
binary representation internally; 

414 

415 
 type nat has special constructor Suc, and generally prefers Suc 0 

416 
over 1::nat and Suc (Suc 0) over 2::nat; 

417 

12364
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

418 
This change may cause significant problems of INCOMPATIBILITY; here 
108cdda23ab3
* Pure/Provers/classical: simplified integration with pure rule
wenzelm
parents:
12335
diff
changeset

419 
are some hints on converting existing sources: 
11702  420 

421 
 due to the new "num" token, "0" and "1" etc. are now atomic 

422 
entities, so expressions involving "" (unary or binary minus) need 

423 
to be spaced properly; 

424 

425 
 existing occurrences of "1" may need to be constraint "1::nat" or 

426 
even replaced by Suc 0; similar for old "2"; 

427 

428 
 replace "#nnn" by "nnn", and "#nnn" by "nnn"; 

429 

430 
 remove all special provisions on numerals in proofs; 

431 

13042  432 
* HOL: simp rules nat_number expand numerals on nat to Suc/0 
12837  433 
representation (depends on bin_arith_simps in the default context); 
434 

12736  435 
* HOL: symbolic syntax for x^2 (numeral 2); 
436 

12335
db4d5f498742
* HOL: the class of all HOL types is now called "type" rather than
wenzelm
parents:
12312
diff
changeset

437 
* HOL: the class of all HOL types is now called "type" rather than 
db4d5f498742
* HOL: the class of all HOL types is now called "type" rather than
wenzelm
parents:
12312
diff
changeset

438 
"term"; INCOMPATIBILITY, need to adapt references to this type class 
db4d5f498742
* HOL: the class of all HOL types is now called "type" rather than
wenzelm
parents:
12312
diff
changeset

439 
in axclass/classes, instance/arities, and (usually rare) occurrences 
db4d5f498742
* HOL: the class of all HOL types is now called "type" rather than
wenzelm
parents:
12312
diff
changeset

440 
in typings (of consts etc.); internally the class is called 
db4d5f498742
* HOL: the class of all HOL types is now called "type" rather than
wenzelm
parents:
12312
diff
changeset

441 
"HOL.type", ML programs should refer to HOLogic.typeS; 
db4d5f498742
* HOL: the class of all HOL types is now called "type" rather than
wenzelm
parents:
12312
diff
changeset

442 

12280  443 
* HOL/record package improvements: 
444 
 new derived operations "fields" to build a partial record section, 

445 
"extend" to promote a fixed record to a record scheme, and 

446 
"truncate" for the reverse; cf. theorems "xxx.defs", which are *not* 

447 
declared as simp by default; 

12587
3f3d2ffb5df5
HOL/record: shared operations ("more", "fields", etc.) now need to be
wenzelm
parents:
12564
diff
changeset

448 
 shared operations ("more", "fields", etc.) now need to be always 
3f3d2ffb5df5
HOL/record: shared operations ("more", "fields", etc.) now need to be
wenzelm
parents:
12564
diff
changeset

449 
qualified)  potential INCOMPATIBILITY; 
12280  450 
 removed "make_scheme" operations (use "make" with "extend")  
451 
INCOMPATIBILITY; 

11937  452 
 removed "more" class (simply use "term")  INCOMPATIBILITY; 
12253  453 
 provides cases/induct rules for use with corresponding Isar 
454 
methods (for concrete records, record schemes, concrete more 

12280  455 
parts, and schematic more parts  in that order); 
11930  456 
 internal definitions directly based on a lightweight abstract 
457 
theory of product types over typedef rather than datatype; 

458 

13023
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

459 
* HOL: generic code generator for generating executable ML code from 
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

460 
specifications; specific support for HOL constructs such as inductive 
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

461 
datatypes and sets, as well as recursive functions; can be invoked 
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

462 
via 'generate_code' theory section; 
f869b6822006
Added two paragraphs on "rules" method and code generator.
berghofe
parents:
12984
diff
changeset

463 

11933  464 
* HOL: canonical cases/induct rules for ntuples (n = 3..7); 
465 

13824  466 
* HOL: consolidated and renamed several theories. In particular: 
467 
Ord.thy has been absorbed into HOL.thy 

468 
String.thy has been absorbed into List.thy 

469 

11802
1d5f5d2427d2
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
wenzelm
parents:
11797
diff
changeset

470 
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" 
1d5f5d2427d2
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
wenzelm
parents:
11797
diff
changeset

471 
(beware of argument permutation!); 
1d5f5d2427d2
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
wenzelm
parents:
11797
diff
changeset

472 

11657  473 
* HOL: linorder_less_split superseded by linorder_cases; 
474 

12917  475 
* HOL/List: "nodups" renamed to "distinct"; 
12889  476 

11633  477 
* HOL: added "The" definite description operator; move Hilbert's "Eps" 
13824  478 
to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES: 
479 
 Ex_def has changed, now need to use some_eq_ex 

11437  480 

11572  481 
* HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so 
482 
in this (rare) case use: 

483 

484 
delSWrapper "split_all_tac" 

485 
addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac) 

486 

487 
* HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS 

11474  488 
MAY FAIL; 
11361  489 

11572  490 
* HOL: introduced f^n = f o ... o f; warning: due to the limits of 
491 
Isabelle's type classes, ^ on functions and relations has too general 

492 
a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be 

493 
necessary to attach explicit type constraints; 

11307  494 

12917  495 
* HOL/Relation: the prefix name of the infix "O" has been changed from 
496 
"comp" to "rel_comp"; INCOMPATIBILITY: a few theorems have been 

497 
renamed accordingly (eg "compI" > "rel_compI"). 

12489  498 

11487
95071c9e85a3
* HOL: syntax translations now work properly with numerals and records
wenzelm
parents:
11475
diff
changeset

499 
* HOL: syntax translations now work properly with numerals and records 
95071c9e85a3
* HOL: syntax translations now work properly with numerals and records
wenzelm
parents:
11475
diff
changeset

500 
expressions; 
11474  501 

12457
cbfc53e45476
* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
wenzelm
parents:
12405
diff
changeset

502 
* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead 
cbfc53e45476
* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
wenzelm
parents:
12405
diff
changeset

503 
of "lam"  INCOMPATIBILITY; 
11474  504 

11933  505 
* HOL: got rid of some global declarations (potential INCOMPATIBILITY 
506 
for ML tools): const "()" renamed "Product_Type.Unity", type "unit" 

507 
renamed "Product_Type.unit"; 

11611  508 

12564  509 
* HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl 
510 

12924  511 
* HOL: removed obsolete theorem "optionE" (use "option.exhaust", or 
512 
the "cases" method); 

513 

12597
14822e4436bf
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
wenzelm
parents:
12587
diff
changeset

514 
* HOL/GroupTheory: group theory examples including Sylow's theorem (by 
14822e4436bf
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
wenzelm
parents:
12587
diff
changeset

515 
Florian Kammüller); 
14822e4436bf
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
wenzelm
parents:
12587
diff
changeset

516 

12608
2df381faa787
* ZF/IMP: updated and converted to newstyle theory format;
wenzelm
parents:
12597
diff
changeset

517 
* HOL/IMP: updated and converted to newstyle theory format; several 
2df381faa787
* ZF/IMP: updated and converted to newstyle theory format;
wenzelm
parents:
12597
diff
changeset

518 
parts turned into readable document, with proper Isar proof texts and 
2df381faa787
* ZF/IMP: updated and converted to newstyle theory format;
wenzelm
parents:
12597
diff
changeset

519 
some explanations (by Gerwin Klein); 
12597
14822e4436bf
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
wenzelm
parents:
12587
diff
changeset

520 

12734  521 
* HOLReal: added Complex_Numbers (by Gertrud Bauer); 
522 

12690  523 
* HOLHyperreal is now a logic image; 
524 

11611  525 

12022
9c3377b133c0
HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
wenzelm
parents:
11995
diff
changeset

526 
*** HOLCF *** 
9c3377b133c0
HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
wenzelm
parents:
11995
diff
changeset

527 

12622  528 
* Isar: consts/constdefs supports mixfix syntax for continuous 
529 
operations; 

530 

531 
* Isar: domain package adapted to newstyle theory format, e.g. see 

532 
HOLCF/ex/Dnat.thy; 

533 

534 
* theory Lift: proper use of rep_datatype lift instead of ML hacks  

12280  535 
potential INCOMPATIBILITY; now use plain induct_tac instead of former 
536 
lift.induct_tac, always use UU instead of Undef; 

12022
9c3377b133c0
HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
wenzelm
parents:
11995
diff
changeset

537 

12597
14822e4436bf
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
wenzelm
parents:
12587
diff
changeset

538 
* HOLCF/IMP: updated and converted to newstyle theory; 
14822e4436bf
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
wenzelm
parents:
12587
diff
changeset

539 

12022
9c3377b133c0
HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
wenzelm
parents:
11995
diff
changeset

540 

11474  541 
*** ZF *** 
542 

12622  543 
* Isar: proper integration of logicspecific tools and packages, 
544 
including theory commands '(co)inductive', '(co)datatype', 

545 
'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', 

546 
'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); 

547 

548 
* theory Main no longer includes AC; for the Axiom of Choice, base 

549 
your theory on Main_ZFC; 

550 

551 
* the integer library now covers quotients and remainders, with many 

552 
laws relating division to addition, multiplication, etc.; 

12563  553 

12280  554 
* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a 
555 
typeless version of the formalism; 

556 

13025  557 
* ZF/AC, Coind, IMP, Resid: updated and converted to newstyle theory 
558 
format; 

12608
2df381faa787
* ZF/IMP: updated and converted to newstyle theory format;
wenzelm
parents:
12597
diff
changeset

559 

12280  560 
* ZF/Induct: new directory for examples of inductive definitions, 
12608
2df381faa787
* ZF/IMP: updated and converted to newstyle theory format;
wenzelm
parents:
12597
diff
changeset

561 
including theory Multiset for multiset orderings; converted to 
2df381faa787
* ZF/IMP: updated and converted to newstyle theory format;
wenzelm
parents:
12597
diff
changeset

562 
newstyle theory format; 
12177
b1c16d685a99
* ZF: newstyle theory commands 'inductive', 'inductive_cases', and
wenzelm
parents:
12163
diff
changeset

563 

13025  564 
* ZF: many new theorems about lists, ordinals, etc.; 
12850  565 

11474  566 

567 
*** General *** 

568 

12280  569 
* Pure/kernel: metalevel proof terms (by Stefan Berghofer); reference 
570 
variable proof controls level of detail: 0 = no proofs (only oracle 

571 
dependencies), 1 = lemma dependencies, 2 = compact proof terms; see 

572 
also ref manual for further ML interfaces; 

573 

574 
* Pure/axclass: removed obsolete ML interface 

575 
goal_subclass/goal_arity; 

576 

577 
* Pure/syntax: new token syntax "num" for plain numerals (without "#" 

578 
of "xnum"); potential INCOMPATIBILITY, since 0, 1 etc. are now 

579 
separate tokens, so expressions involving minus need to be spaced 

580 
properly; 

581 

12312
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

582 
* Pure/syntax: support nonoriented infixes, using keyword "infix" 
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

583 
rather than "infixl" or "infixr"; 
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

584 

f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

585 
* Pure/syntax: concrete syntax for dummy type variables admits genuine 
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

586 
sort constraint specifications in type inference; e.g. "x::_::foo" 
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

587 
ensures that the type of "x" is of sort "foo" (but not necessarily a 
f0f06950820d
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
wenzelm
parents:
12280
diff
changeset

588 
type variable); 
12280  589 

590 
* Pure/syntax: print modes "type_brackets" and "no_type_brackets" 

591 
control output of nested => (types); the default behavior is 

592 
"type_brackets"; 

593 

594 
* Pure/syntax: builtin parse translation for "_constify" turns valued 

11817  595 
tokens into AST constants; 
11474  596 

12280  597 
* Pure/syntax: prefer later declarations of translations and print 
598 
translation functions; potential INCOMPATIBILITY: need to reverse 

599 
multiple declarations for same syntax element constant; 

600 

12832
c31b44286a8a
* Pure/show_hyps reset by default (in accordance to existing Isar practice);
wenzelm
parents:
12777
diff
changeset

601 
* Pure/show_hyps reset by default (in accordance to existing Isar 
c31b44286a8a
* Pure/show_hyps reset by default (in accordance to existing Isar practice);
wenzelm
parents:
12777
diff
changeset

602 
practice); 
c31b44286a8a
* Pure/show_hyps reset by default (in accordance to existing Isar practice);
wenzelm
parents:
12777
diff
changeset

603 

12280  604 
* Provers/classical: renamed addaltern to addafter, addSaltern to 
605 
addSafter; 

606 

607 
* Provers/clasimp: ``iff'' declarations now handle conditional rules 

608 
as well; 

12253  609 

12538  610 
* system: tested support for MacOS X; should be able to get Isabelle + 
611 
Proof General to work in a plain Terminal after installing Poly/ML 

612 
(e.g. from the Isabelle distribution area) and GNU bash alone 

613 
(e.g. from http://www.apple.com); full X11, XEmacs and XSymbol 

614 
support requires further installations, e.g. from 

615 
http://fink.sourceforge.net/); 

616 

12280  617 
* system: support Poly/ML 4.1.1 (able to manage larger heaps); 
11551  618 

12753
3a62df7ae926
* system: reduced base memory usage by Poly/ML (approx. 20 MB instead
wenzelm
parents:
12736
diff
changeset

619 
* system: reduced base memory usage by Poly/ML (approx. 20 MB instead 
3a62df7ae926
* system: reduced base memory usage by Poly/ML (approx. 20 MB instead
wenzelm
parents:
12736
diff
changeset

620 
of 40 MB), cf. ML_OPTIONS; 
3a62df7ae926
* system: reduced base memory usage by Poly/ML (approx. 20 MB instead
wenzelm
parents:
12736
diff
changeset

621 

11633  622 
* system: Proof General keywords specification is now part of the 
623 
Isabelle distribution (see etc/isarkeywords.el); 

624 

12728  625 
* system: support for persistent Proof General sessions (refrain from 
626 
outdating all loaded theories on startup); user may create writable 

627 
logic images like this: ``isabelle q HOL Test''; 

12597
14822e4436bf
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
wenzelm
parents:
12587
diff
changeset

628 

11551  629 
* system: smart selection of Isabelle process versus Isabelle 
11572  630 
interface, accommodates caseinsensitive file systems (e.g. HFS+); may 
631 
run both "isabelle" and "Isabelle" even if file names are badly 

632 
damaged (executable inspects the case of the first letter of its own 

633 
name); added separate "isabelleprocess" and "isabelleinterface"; 

11551  634 

12472  635 
* system: refrain from any attempt at filtering input streams; no 
636 
longer support ``8bit'' encoding of old isabelle font, instead proper 

637 
isolatin characters may now be used; the related isatools 

638 
"symbolinput" and "nonascii" have disappeared as well; 

639 

640 
* system: removed old "xterm" interface (the print modes "xterm" and 

641 
"xterm_color" are still available for direct use in a suitable 

642 
terminal); 

643 

11314  644 

11169
98c2f741e32b
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
oheimb
parents:
11130
diff
changeset

645 

11062  646 
New in Isabelle992 (February 2001) 
647 
 

648 

10224  649 
*** Overview of INCOMPATIBILITIES *** 
650 

11241  651 
* HOL: please note that theories in the Library and elsewhere often use the 
652 
newstyle (Isar) format; to refer to their theorems in an ML script you must 

12622  653 
bind them to ML identifers by e.g. val thm_name = thm "thm_name"; 
11241  654 

11043
2e3bbac8763b
HOL: inductive package no longer splits induction rule aggressively,
wenzelm
parents:
11016
diff
changeset

655 
* HOL: inductive package no longer splits induction rule aggressively, 
2e3bbac8763b
HOL: inductive package no longer splits induction rule aggressively,
wenzelm
parents:
11016
diff
changeset

656 
but only as far as specified by the introductions given; the old 
11130  657 
format may be recovered via ML function complete_split_rule or attribute 
11043
2e3bbac8763b
HOL: inductive package no longer splits induction rule aggressively,
wenzelm
parents:
11016
diff
changeset

658 
'split_rule (complete)'; 
2e3bbac8763b
HOL: inductive package no longer splits induction rule aggressively,
wenzelm
parents:
11016
diff
changeset

659 

10998  660 
* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, 
661 
gfp_Tarski to gfp_unfold; 

10224  662 

10288  663 
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; 
664 

10858  665 
* HOL: infix "dvd" now has priority 50 rather than 70 (because it is a 
666 
relation); infix "^^" has been renamed "``"; infix "``" has been 

667 
renamed "`"; "univalent" has been renamed "single_valued"; 

10793  668 

10998  669 
* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" 
670 
operation; 

671 

10868  672 
* HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>; 
10856  673 

10391  674 
* Isar: 'obtain' no longer declares "that" fact as simp/intro; 
675 

10401
58bb50f69497
* Isar/HOL: method 'induct' now handles nonatomic goals; as a
wenzelm
parents:
10391
diff
changeset

676 
* Isar/HOL: method 'induct' now handles nonatomic goals; as a 
58bb50f69497
* Isar/HOL: method 'induct' now handles nonatomic goals; as a
wenzelm
parents:
10391
diff
changeset

677 
consequence, it is no longer monotonic wrt. the local goal context 
58bb50f69497
* Isar/HOL: method 'induct' now handles nonatomic goals; as a
wenzelm
parents:
10391
diff
changeset

678 
(which is now passed through the inductive cases); 
58bb50f69497
* Isar/HOL: method 'induct' now handles nonatomic goals; as a
wenzelm
parents:
10391
diff
changeset

679 

10976
0e7cf6f9fa29
* Document preparation: renamed standard symbols \<ll> to \<lless> and
wenzelm
parents:
10966
diff
changeset

680 
* Document preparation: renamed standard symbols \<ll> to \<lless> and 
0e7cf6f9fa29
* Document preparation: renamed standard symbols \<ll> to \<lless> and
wenzelm
parents:
10966
diff
changeset

681 
\<gg> to \<ggreater>; 
0e7cf6f9fa29
* Document preparation: renamed standard symbols \<ll> to \<lless> and
wenzelm
parents:
10966
diff
changeset

682 

10224  683 

10245
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

684 
*** Document preparation *** 
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

685 

10858  686 
* \isabellestyle{NAME} selects version of Isabelle output (currently 
687 
available: are "it" for near mathmode beststyle output, "sl" for 

688 
slanted text style, and "tt" for plain typewriter; if no 

689 
\isabellestyle command is given, output is according to slanted 

690 
typewriter); 

691 

10322
df38c61bf541
* support sub/super scripts (for single symbols only), input syntax is
wenzelm
parents:
10306
diff
changeset

692 
* support sub/super scripts (for single symbols only), input syntax is 
df38c61bf541
* support sub/super scripts (for single symbols only), input syntax is
wenzelm
parents:
10306
diff
changeset

693 
like this: "A\<^sup>*" or "A\<^sup>\<star>"; 
df38c61bf541
* support sub/super scripts (for single symbols only), input syntax is
wenzelm
parents:
10306
diff
changeset

694 

10858  695 
* some more standard symbols; see Appendix A of the system manual for 
11062  696 
the complete list of symbols defined in isabellesym.sty; 
10858  697 

10998  698 
* improved isabelle style files; more abstract symbol implementation 
699 
(should now use \isamath{...} and \isatext{...} in custom symbol 

700 
definitions); 

701 

10634  702 
* antiquotation @{goals} and @{subgoals} for output of *dynamic* goals 
703 
state; Note that presentation of goal states does not conform to 

704 
actual humanreadable proof documents. Please do not include goal 

705 
states into document output unless you really know what you are doing! 

10322
df38c61bf541
* support sub/super scripts (for single symbols only), input syntax is
wenzelm
parents:
10306
diff
changeset

706 

11062  707 
* proper indentation of antiquoted output with proportional LaTeX 
708 
fonts; 

10862  709 

11050
ac5709ac50b9
* no_document ML operator temporarily disables LaTeX document
wenzelm
parents:
11043
diff
changeset

710 
* no_document ML operator temporarily disables LaTeX document 
ac5709ac50b9
* no_document ML operator temporarily disables LaTeX document
wenzelm
parents:
11043
diff
changeset

711 
generation; 
ac5709ac50b9
* no_document ML operator temporarily disables LaTeX document
wenzelm
parents:
11043
diff
changeset

712 

11062  713 
* isatool unsymbolize tunes sources for plain ASCII communication; 
714 

10322
df38c61bf541
* support sub/super scripts (for single symbols only), input syntax is
wenzelm
parents:
10306
diff
changeset

715 

10306
b0ab988a27a9
* HOL: default proof step now includes 'intro_classes';
wenzelm
parents:
10288
diff
changeset

716 
*** Isar *** 
b0ab988a27a9
* HOL: default proof step now includes 'intro_classes';
wenzelm
parents:
10288
diff
changeset

717 

10547  718 
* Pure: Isar now suffers initial goal statements to contain unbound 
719 
schematic variables (this does not conform to actual readable proof 

720 
documents, due to unpredictable outcome and noncompositional proof 

721 
checking); users who know what they are doing may use schematic goals 

722 
for Prologstyle synthesis of proven results; 

723 

10391  724 
* Pure: assumption method (an implicit finishing) now handles actual 
725 
rules as well; 

726 

727 
* Pure: improved 'obtain'  moved to Pure, insert "that" into 

728 
initial goal, declare "that" only as Pure intro (only for single 

729 
steps); the "that" rule assumption may now be involved in implicit 

730 
finishing, thus ".." becomes a feasible for trivial obtains; 

731 

732 
* Pure: default proof step now includes 'intro_classes'; thus trivial 

733 
instance proofs may be performed by ".."; 

734 

735 
* Pure: ?thesis / ?this / "..." now work for pure metalevel 

736 
statements as well; 

10306
b0ab988a27a9
* HOL: default proof step now includes 'intro_classes';
wenzelm
parents:
10288
diff
changeset

737 

11097  738 
* Pure: more robust selection of calculational rules; 
739 

10858  740 
* Pure: the builtin notion of 'finished' goal now includes the ==refl 
741 
rule (as well as the assumption rule); 

742 

743 
* Pure: 'thm_deps' command visualizes dependencies of theorems and 

744 
lemmas, using the graph browser tool; 

745 

10944  746 
* Pure: predict failure of "show" in interactive mode; 
747 

11016
8f8ba41a5e7a
* Pure: 'thms_containing' now takes actual terms as arguments;
wenzelm
parents:
10998
diff
changeset

748 
* Pure: 'thms_containing' now takes actual terms as arguments; 
8f8ba41a5e7a
* Pure: 'thms_containing' now takes actual terms as arguments;
wenzelm
parents:
10998
diff
changeset

749 

10401
58bb50f69497
* Isar/HOL: method 'induct' now handles nonatomic goals; as a
wenzelm
parents:
10391
diff
changeset

750 
* HOL: improved method 'induct'  now handles nonatomic goals 
58bb50f69497
* Isar/HOL: method 'induct' now handles nonatomic goals; as a
wenzelm
parents:
10391
diff
changeset

751 
(potential INCOMPATIBILITY); tuned error handling; 
58bb50f69497
* Isar/HOL: method 'induct' now handles nonatomic goals; as a
wenzelm
parents:
10391
diff
changeset

752 

10557  753 
* HOL: cases and induct rules now provide explicit hints about the 
10547  754 
number of facts to be consumed (0 for "type" and 1 for "set" rules); 
755 
any remaining facts are inserted into the goal verbatim; 

756 

10858  757 
* HOL: local contexts (aka cases) may now contain term bindings as 
758 
well; the 'cases' and 'induct' methods new provide a ?case binding for 

759 
the result to be shown in each case; 

760 

10770  761 
* HOL: added 'recdef_tc' command; 
762 

11016
8f8ba41a5e7a
* Pure: 'thms_containing' now takes actual terms as arguments;
wenzelm
parents:
10998
diff
changeset

763 
* isatool convert assists in eliminating legacy ML scripts; 
8f8ba41a5e7a
* Pure: 'thms_containing' now takes actual terms as arguments;
wenzelm
parents:
10998
diff
changeset

764 

10306
b0ab988a27a9
* HOL: default proof step now includes 'intro_classes';
wenzelm
parents:
10288
diff
changeset

765 

10245
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

766 
*** HOL *** 
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

767 

87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

768 
* HOL/Library: a collection of generic theories to be used together 
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

769 
with main HOL; the theory loader path already includes this directory 
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

770 
by default; the following existing theories have been moved here: 
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

771 
HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While 
10337  772 
(as While_Combinator), HOL/Lex/Prefix (as List_Prefix); 
10245
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

773 

10966  774 
* HOL/Unix: "Some aspects of Unix filesystem security", a typical 
775 
modelling and verification task performed in Isabelle/HOL + 

776 
Isabelle/Isar + Isabelle document preparation (by Markus Wenzel). 

777 

11094  778 
* HOL/Algebra: special summation operator SUM no longer exists, it has 
779 
been replaced by setsum; infix 'assoc' now has priority 50 (like 

780 
'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to 

781 
'domain', this makes the theory consistent with mathematical 

782 
literature; 

783 

10514  784 
* HOL basics: added overloaded operations "inverse" and "divide" 
10726  785 
(infix "/"), syntax for generic "abs" operation, generic summation 
11094  786 
operator \<Sum>; 
10452
abeefb0a79ae
* added overloaded operations "inverse" and "divide" (infix "/");
wenzelm
parents:
10428
diff
changeset

787 

10391  788 
* HOL/typedef: simplified package, provide more useful rules (see also 
789 
HOL/subset.thy); 

790 

10915
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

791 
* HOL/datatype: induction rule for arbitrarily branching datatypes is 
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

792 
now expressed as a proper nested rule (oldstyle tactic scripts may 
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

793 
require atomize_strip_tac to cope with nonatomic premises); 
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

794 

6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

795 
* HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule 
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

796 
to "split_conv" (old name still available for compatibility); 
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

797 

6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

798 
* HOL: improved concrete syntax for strings (e.g. allows translation 
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

799 
rules with string literals); 
6b66a8a530ce
* HOL/datatype: induction rule for arbitrarily branching datatypes is
wenzelm
parents:
10868
diff
changeset

800 

12245  801 
* HOLRealHyperreal: this extends HOLReal with the hyperreals 
802 
and Fleuriot's mechanization of analysis, including the transcendental 

803 
functions for the reals; 

10756  804 

11094  805 
* HOL/Real, HOL/Hyperreal: improved arithmetic simplification; 
10391  806 

10858  807 

10474  808 
*** CTT *** 
809 

10547  810 
* CTT: xsymbol support for Pi, Sigma, >, : (membership); note that 
811 
"lam" is displayed as TWO lambdasymbols 

10474  812 

10547  813 
* CTT: theory Main now available, containing everything (that is, Bool 
814 
and Arith); 

815 

10474  816 

10391  817 
*** General *** 
818 

10547  819 
* Pure: the Simplifier has been implemented properly as a derived rule 
820 
outside of the actual kernel (at last!); the overall performance 

821 
penalty in practical applications is about 50%, while reliability of 

822 
the Isabelle inference kernel has been greatly improved; 

823 

11112  824 
* print modes "brackets" and "no_brackets" control output of nested => 
825 
(types) and ==> (props); the default behaviour is "brackets"; 

826 

10391  827 
* Provers: fast_tac (and friends) now handle actual objectlogic rules 
828 
as assumptions as well; 

829 

11124  830 
* system: support Poly/ML 4.0; 
831 

832 
* system: isatool install handles KDE version 1 or 2; 

833 

10391  834 

10245
87771e2f49fe
* HOL/Library: a collection of generic theories to be used together
wenzelm
parents:
10224
diff
changeset

835 

10103  836 
New in Isabelle991 (October 2000) 
837 
 

8015  838 

10003  839 
*** Overview of INCOMPATIBILITIES *** 
8014  840 

8848  841 
* HOL: simplification of natural numbers is much changed; to partly 
842 
recover the old behaviour (e.g. to prevent n+n rewriting to #2*n) 

843 
issue the following ML commands: 

844 

845 
Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; 

846 
Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; 

8788  847 

10129  848 
* HOL: simplification no longer dives into caseexpressions; this is 
849 
controlled by "t.weak_case_cong" for each datatype t; 

10003  850 

851 
* HOL: nat_less_induct renamed to less_induct; 

852 

853 
* HOL: systematic renaming of the SOME (Eps) rules, may use isatool 

854 
fixsome to patch .thy and .ML sources automatically; 

8967  855 

10003  856 
select_equality > some_equality 
857 
select_eq_Ex > some_eq_ex 

858 
selectI2EX > someI2_ex 

859 
selectI2 > someI2 

860 
selectI > someI 

861 
select1_equality > some1_equality 

862 
Eps_sym_eq > some_sym_eq_trivial 

863 
Eps_eq > some_eq_trivial 

864 

865 
* HOL: exhaust_tac on datatypes superceded by new generic case_tac; 

866 

867 
* HOL: removed obsolete theorem binding expand_if (refer to split_if 

868 
instead); 

869 

870 
* HOL: the recursion equations generated by 'recdef' are now called 

871 
f.simps instead of f.rules; 

872 

873 
* HOL: qed_spec_mp now also handles bounded ALL as well; 

874 

875 
* HOL: 0 is now overloaded, so the type constraint ":: nat" may 

876 
sometimes be needed; 

877 

878 
* HOL: the constant for "f``x" is now "image" rather than "op ``"; 

8014  879 

10065  880 
* HOL: the constant for "f``x" is now "vimage" rather than "op ``"; 
881 

9330
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

882 
* HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian 
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

883 
product is now "<*>" instead of "Times"; the lexicographic product is 
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

884 
now "<*lex*>" instead of "**"; 
8705  885 

10003  886 
* HOL: theory Sexp is now in HOL/Induct examples (it used to be part 
887 
of main HOL, but was unused); better use HOL's datatype package; 

9971  888 

10137
d1c2bef01e2f
removed "symbols" syntax for constant "override";
wenzelm
parents:
10129
diff
changeset

889 
* HOL: removed "symbols" syntax for constant "override" of theory Map; 
d1c2bef01e2f
removed "symbols" syntax for constant "override";
wenzelm
parents:
10129
diff
changeset

890 
the old syntax may be recovered as follows: 
d1c2bef01e2f
removed "symbols" syntax for constant "override";
wenzelm
parents:
10129
diff
changeset

891 

d1c2bef01e2f
removed "symbols" syntax for constant "override";
wenzelm
parents:
10129
diff
changeset

892 
syntax (symbols) 
d1c2bef01e2f
removed "symbols" syntax for constant "override";
wenzelm
parents:
10129
diff
changeset

893 
override :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" 
d1c2bef01e2f
removed "symbols" syntax for constant "override";
wenzelm
parents:
10129
diff
changeset

894 
(infixl "\\<oplus>" 100) 
d1c2bef01e2f
removed "symbols" syntax for constant "override";
wenzelm
parents:
10129
diff
changeset

895 

8848  896 
* HOL/Real: "rabs" replaced by overloaded "abs" function; 
897 

8887
c0c583ce0b0b
* HOL/ML: even fewer consts are declared as global (see theories Ord,
wenzelm
parents:
8848
diff
changeset

898 
* HOL/ML: even fewer consts are declared as global (see theories Ord, 
c0c583ce0b0b
* HOL/ML: even fewer consts are declared as global (see theories Ord,
wenzelm
parents:
8848
diff
changeset

899 
Lfp, Gfp, WF); this only affects ML packages that refer to const names 
c0c583ce0b0b
* HOL/ML: even fewer consts are declared as global (see theories Ord,
wenzelm
parents:
8848
diff
changeset

900 
internally; 
c0c583ce0b0b
* HOL/ML: even fewer consts are declared as global (see theories Ord,
wenzelm
parents:
8848
diff
changeset

901 

10003  902 
* HOL and ZF: syntax for quotienting wrt an equivalence relation 
903 
changed from A/r to A//r; 

9908  904 

10003  905 
* ZF: new treatment of arithmetic (nat & int) may break some old 
906 
proofs; 

8921
7c04c98132c4
* Pure: changed syntax of local blocks from {{ }} to { };
wenzelm
parents:
8887
diff
changeset

907 

10003  908 
* Isar: renamed some attributes (RS > THEN, simplify > simplified, 
909 
rulify > rule_format, elimify > elim_format, ...); 

9542  910 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

911 
* Isar/Provers: intro/elim/dest attributes changed; renamed 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

912 
intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one 
9937  913 
should have to change intro!! to intro? only); replaced "delrule" by 
914 
"rule del"; 

9437
93e91040c286
* Isar/Provers: intro/elim/dest attributes: changed
wenzelm
parents:
9402
diff
changeset

915 

9612  916 
* Isar/HOL: renamed "intrs" to "intros" in inductive definitions; 
917 

9437
93e91040c286
* Isar/Provers: intro/elim/dest attributes: changed
wenzelm
parents:
9402
diff
changeset

918 
* Provers: strengthened force_tac by using new first_best_tac; 
9402  919 

10003  920 
* LaTeX document preparation: several changes of isabelle.sty (see 
921 
lib/texinputs); 

8729
094dbd0fad0c
* improved name spaces: ambiguous output is qualified; support for
wenzelm
parents:
8705
diff
changeset

922 

8014  923 

8487  924 
*** Document preparation *** 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

925 

9198
0ab3c81e9425
* formal comments (text blocks etc.) in newstyle theories may now
wenzelm
parents:
9185
diff
changeset

926 
* formal comments (text blocks etc.) in newstyle theories may now 
9753  927 
contain antiquotations of thm/prop/term/typ/text to be presented 
928 
according to latex print mode; concrete syntax is like this: 

929 
@{term[show_types] "f(x) = a + x"}; 

9198
0ab3c81e9425
* formal comments (text blocks etc.) in newstyle theories may now
wenzelm
parents:
9185
diff
changeset

930 

8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

931 
* isatool mkdir provides easy setup of Isabelle session directories, 
8518  932 
including proper document sources; 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

933 

a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

934 
* generated LaTeX sources are now deleted after successful run 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

935 
(isatool document c); may retain a copy somewhere else via D option 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

936 
of isatool usedir; 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

937 

8566  938 
* isatool usedir D now lets isatool latex o sty update the Isabelle 
10003  939 
style files, achieving selfcontained LaTeX sources and simplifying 
940 
LaTeX debugging; 

8566  941 

8518  942 
* oldstyle theories now produce (crude) LaTeX output as well; 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

943 

9057
af1ca1acf292
* browser info session directories are now selfcontained (may be put
wenzelm
parents:
9052
diff
changeset

944 
* browser info session directories are now selfcontained (may be put 
9437
93e91040c286
* Isar/Provers: intro/elim/dest attributes: changed
wenzelm
parents:
9402
diff
changeset

945 
on WWW server seperately); improved graphs of nested sessions; removed 
93e91040c286
* Isar/Provers: intro/elim/dest attributes: changed
wenzelm
parents:
9402
diff
changeset

946 
graph for 'all sessions'; 
9057
af1ca1acf292
* browser info session directories are now selfcontained (may be put
wenzelm
parents:
9052
diff
changeset

947 

10003  948 
* several improvements in isabelle style files; \isabellestyle{it} 
949 
produces fake math mode output; \isamarkupheader is now \section by 

950 
default; see lib/texinputs/isabelle.sty etc.; 

9489
aa757b35b129
* blast(_tac) now handles actual objectlogic rules as assumptions;
wenzelm
parents:
9457
diff
changeset

951 

8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

952 

8184  953 
*** Isar *** 
954 

10003  955 
* Isar/Pure: local results and corresponding term bindings are now 
956 
subject to HindleyMilner polymorphism (similar to ML); this 

957 
accommodates incremental typeinference very nicely; 

8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

958 

10003  959 
* Isar/Pure: new derived language element 'obtain' supports 
960 
generalized existence reasoning; 

8621
8ba0f90f6f35
* Isar/Pure: local results and corresponding term bindings are now
wenzelm
parents:
8603
diff
changeset

961 

10003  962 
* Isar/Pure: new calculational elements 'moreover' and 'ultimately' 
963 
support accumulation of results, without applying any rules yet; 

964 
useful to collect intermediate results without explicit name 

965 
references, and for use with transitivity rules with more than 2 

966 
premises; 

8184  967 

10003  968 
* Isar/Pure: scalable support for caseanalysis type proofs: new 
969 
'case' language element refers to local contexts symbolically, as 

970 
produced by certain proof methods; internally, case names are attached 

971 
to theorems as "tags"; 

8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

972 

10003  973 
* Isar/Pure: theory command 'hide' removes declarations from 
9330
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

974 
class/type/const name spaces; 
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

975 

10003  976 
* Isar/Pure: theory command 'defs' supports option "(overloaded)" to 
9330
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

977 
indicate potential overloading; 
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

978 

10003  979 
* Isar/Pure: changed syntax of local blocks from {{ }} to { }; 
8621
8ba0f90f6f35
* Isar/Pure: local results and corresponding term bindings are now
wenzelm
parents:
8603
diff
changeset

980 

10003  981 
* Isar/Pure: syntax of sorts made 'inner', i.e. have to write 
982 
"{a,b,c}" instead of {a,b,c}; 

9011
0cfc347f8d19
Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to
wenzelm
parents:
8994
diff
changeset

983 

10003  984 
* Isar/Pure now provides its own version of intro/elim/dest 
985 
attributes; useful for building new logics, but beware of confusion 

986 
with the version in Provers/classical; 

9612  987 

10003  988 
* Isar/Pure: the local context of (nonatomic) goals is provided via 
989 
case name 'antecedent'; 

8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

990 

10003  991 
* Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms 
992 
to the current context is now done automatically); 

9383
c21fa1c48de0
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
wenzelm
parents:
9349
diff
changeset

993 

10003  994 
* Isar/Pure: theory command 'method_setup' provides a simple interface 
995 
for definining proof methods in ML; 

9612  996 

10003  997 
* Isar/Provers: intro/elim/dest attributes changed; renamed 
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

998 
intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

999 
most cases, one should have to change intro!! to intro? only); 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

1000 
replaced "delrule" by "rule del"; 
8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

1001 

10003  1002 
* Isar/Provers: new 'hypsubst' method, plain 'subst' method and 
1003 
'symmetric' attribute (the latter supercedes [RS sym]); 

1004 

1005 
* Isar/Provers: splitter support (via 'split' attribute and 'simp' 

1006 
method modifier); 'simp' method: 'only:' modifier removes loopers as 

1007 
well (including splits); 

1008 

1009 
* Isar/Provers: Simplifier and Classical methods now support all kind 

1010 
of modifiers used in the past, including 'cong', 'iff', etc. 

1011 

1012 
* Isar/Provers: added 'fastsimp' and 'clarsimp' methods (combination 

1013 
of Simplifier and Classical reasoner); 

1014 

1015 
* Isar/HOL: new proof method 'cases' and improved version of 'induct' 

1016 
now support named cases; major packages (inductive, datatype, primrec, 

1017 
recdef) support case names and properly name parameters; 

9612  1018 

10003  1019 
* Isar/HOL: new transitivity rules for substitution in inequalities  
1020 
monotonicity conditions are extracted to be proven at end of 

1021 
calculations; 

1022 

1023 
* Isar/HOL: removed 'case_split' thm binding, should use 'cases' proof 

1024 
method anyway; 

1025 

1026 
* Isar/HOL: removed old expand_if = split_if; theorems if_splits = 

1027 
split_if split_if_asm; datatype package provides theorems foo.splits = 

1028 
foo.split foo.split_asm for each datatype; 

1029 

1030 
* Isar/HOL: tuned inductive package, rename "intrs" to "intros" 

1031 
(potential INCOMPATIBILITY), emulation of mk_cases feature for proof 

1032 
scripts: new 'inductive_cases' command and 'ind_cases' method; (Note: 

1033 
use "(cases (simplified))" method in proper proof texts); 

1034 

1035 
* Isar/HOL: added global 'arith_split' attribute for 'arith' method; 

1036 

1037 
* Isar: names of theorems etc. may be natural numbers as well; 

1038 

1039 
* Isar: 'pr' command: optional arguments for goals_limit and 

9724
2030c5d63741
* 'pr' command: optional argument for ProofContext.prems_limit;
wenzelm
parents:
9709
diff
changeset

1040 
ProofContext.prems_limit; no longer prints theory contexts, but only 
2030c5d63741
* 'pr' command: optional argument for ProofContext.prems_limit;
wenzelm
parents:
9709
diff
changeset

1041 
proof states; 
8487  1042 

10003  1043 
* Isar: diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit 
8518  1044 
additional print modes to be specified; e.g. "pr(latex)" will print 
1045 
proof state according to the Isabelle LaTeX style; 

8487  1046 

10003  1047 
* Isar: improved support for emulating tactic scripts, including proof 
9612  1048 
methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac', 
1049 
'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac' 

1050 
(for HOL datatypes); 

8534  1051 

10003  1052 
* Isar: simplified (more robust) goal selection of proof methods: 1st 
1053 
goal, all goals, or explicit goal specifier (tactic emulation); thus 

1054 
'proof method scripts' have to be in depthfirst order; 

8673
987ea1a559d0
Isar: simplified (more robust) goal selection of proof methods;
wenzelm
parents:
8655
diff
changeset

1055 

10003  1056 
* Isar: tuned 'let' syntax: replaced 'as' keyword by 'and'; 
8729
094dbd0fad0c
* improved name spaces: ambiguous output is qualified; support for
wenzelm
parents:
8705
diff
changeset

1057 

10003  1058 
* Isar: removed 'help' command, which hasn't been too helpful anyway; 
1059 
should instead use individual commands for printing items 

1060 
(print_commands, print_methods etc.); 

9224
0da360494917
* Isar: removed 'help' command, which hasn't been too helpful anyway;
wenzelm
parents:
9198
diff
changeset

1061 

10003  1062 
* Isar: added 'nothing'  the empty list of theorems; 
9239  1063 

8184  1064 

8014  1065 
*** HOL *** 
1066 

10080  1067 
* HOL/MicroJava: formalization of a fragment of Java, together with a 
1068 
corresponding virtual machine and a specification of its bytecode 

1069 
verifier and a lightweight bytecode verifier, including proofs of 

1070 
typesafety; by Gerwin Klein, Tobias Nipkow, David von Oheimb, and 

1071 
Cornelia Pusch (see also the homepage of project Bali at 

1072 
http://isabelle.in.tum.de/Bali/); 

1073 

8518  1074 
* HOL/Algebra: new theory of rings and univariate polynomials, by 
1075 
Clemens Ballarin; 

8014  1076 

10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1077 
* HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese 
10003  1078 
Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M 
1079 
Rasmussen; 

8570  1080 

10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1081 
* HOL/Lattice: fundamental concepts of lattice theory and order 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1082 
structures, including duals, properties of bounds versus algebraic 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1083 
laws, lattice operations versus settheoretic ones, the KnasterTarski 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1084 
Theorem for complete lattices etc.; may also serve as a demonstration 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1085 
for abstract algebraic reasoning using axiomatic type classes, and 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1086 
mathematicsstyle proof in Isabelle/Isar; by Markus Wenzel; 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10137
diff
changeset

1087 

10003  1088 
* HOL/Prolog: a (barebones) implementation of LambdaProlog, by David 
1089 
von Oheimb; 

9542  1090 

10164
c240747082aa
* HOL/IMPP: extension of IMP with local variables and mutually
wenzelm
parents:
10157
diff
changeset

1091 
* HOL/IMPP: extension of IMP with local variables and mutually 
c240747082aa
* HOL/IMPP: extension of IMP with local variables and mutually
wenzelm
parents:
10157
diff
changeset

1092 
recursive procedures, by David von Oheimb; 
c240747082aa
* HOL/IMPP: extension of IMP with local variables and mutually
wenzelm
parents:
10157
diff
changeset

1093 

10003  1094 
* HOL/Lambda: converted into newstyle theory and document; 
9542  1095 

10003  1096 
* HOL/ex/Multiquote: example of multiple nested quotations and 
1097 
antiquotations  basically a generalized version of deBruijn 

1098 
representation; very useful in avoiding lifting of operations; 

8848  1099 

9612  1100 
* HOL/record: added general record equality rule to simpset; fixed 
1101 
selectupdate simplification procedure to handle extended records as 

1102 
well; admit "r" as field name; 

9542  1103 

8967  1104 
* HOL: 0 is now overloaded over the new sort "zero", allowing its use with 
1105 
other numeric types and also as the identity of groups, rings, etc.; 

1106 

1107 
* HOL: new axclass plus_ac0 for addition with the AClaws and 0 as identity. 

1108 
Types nat and int belong to this axclass; 

1109 

10003  1110 
* HOL: greatly improved simplification involving numerals of type nat, int, real: 
8788  1111 
(i + #8 + j) = Suc k simplifies to #7 + (i + j) = k 
8832  1112 
i*j + k + j*#3*i simplifies to #4*(i*j) + k 
1113 
two terms #m*u and #n*u are replaced by #(m+n)*u 

1114 
(where #m, #n and u can implicitly be 1; this is simproc combine_numerals) 

1115 
and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(mn)+x ~~ y 

1116 
or x ~~ #(nm)+y, where ~~ is one of = < <= or  (simproc cancel_numerals); 

8736  1117 

10003  1118 
* HOL: meson_tac is available (previously in ex/meson.ML); it is a 
1119 
powerful prover for predicate logic but knows nothing of clasets; see 

1120 
ex/mesontest.ML and ex/mesontest2.ML for example applications; 

9835  1121 

8848  1122 
* HOL: new version of "case_tac" subsumes both boolean case split and 
8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

1123 
"exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer 
8518  1124 
exists, may define val exhaust_tac = case_tac for adhoc portability; 
8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

1125 

8848  1126 
* HOL: simplification no longer dives into caseexpressions: only the 
10129  1127 
selector expression is simplified, but not the remaining arms; to 
1128 
enable full simplification of caseexpressions for datatype t, you may 

1129 
remove t.weak_case_cong from the simpset, either globally (Delcongs 

1130 
[thm"t.weak_case_cong"];) or locally (delcongs [...]). 

8603  1131 

8848  1132 
* HOL/recdef: the recursion equations generated by 'recdef' for 
1133 
function 'f' are now called f.simps instead of f.rules; if all 

1134 
termination conditions are proved automatically, these simplification 

1135 
rules are added to the simpset, as in primrec; rules may be named 

1136 
individually as well, resulting in a separate list of theorems for 

1137 
each equation; 

1138 

9489
aa757b35b129
* blast(_tac) now handles actual objectlogic rules as assumptions;
wenzelm
parents:
9457
diff
changeset

1139 
* HOL/While is a new theory that provides a whilecombinator. It 
aa757b35b129
* blast(_tac) now handles actual objectlogic rules as assumptions;
wenzelm
parents:
9457
diff
changeset

1140 
permits the definition of tailrecursive functions without the 
aa757b35b129
* blast(_tac) now handles actual objectlogic rules as assumptions;
wenzelm
parents:
9457
diff
changeset

1141 
provision of a termination measure. The latter is necessary once the 
aa757b35b129
* blast(_tac) now handles actual objectlogic rules as assumptions;
wenzelm
parents:
9457
diff
changeset

1142 
invariant proof rule for while is applied. 
9457  1143 

10003  1144 
* HOL: new (overloaded) notation for the set of elements below/above 
1145 
some element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval. 

8925  1146 

8848  1147 
* HOL: theorems impI, allI, ballI bound as "strip"; 
1148 

10003  1149 
* HOL: new tactic induct_thm_tac: thm > string > int > tactic 
9746  1150 
induct_tac th "x1 ... xn" expects th to have a conclusion of the form 
1151 
P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th; 

1152 

10003  1153 
* HOL/Real: "rabs" replaced by overloaded "abs" function; 
9737  1154 

10003  1155 
* HOL: theory Sexp now in HOL/Induct examples (it used to be part of 
1156 
main HOL, but was unused); 

8626  1157 

10003  1158 
* HOL: fewer consts declared as global (e.g. have to refer to 
1159 
"Lfp.lfp" instead of "lfp" internally; affects ML packages only); 

8887
c0c583ce0b0b
* HOL/ML: even fewer consts are declared as global (see theories Ord,
wenzelm
parents:
8848
diff
changeset

1160 

10003  1161 
* HOL: tuned AST representation of nested pairs, avoiding bogus output 
1162 
in case of overlap with user translations (e.g. judgements over 

1163 
tuples); (note that the underlying logical represenation is still 

1164 
bogus); 

9349
d43669fb423d
* tuned AST representation of nested pairs, avoiding bogus output in
wenzelm
parents:
9335
diff
changeset

1165 

8412  1166 

9542  1167 
*** ZF *** 
1168 

10003  1169 
* ZF: simplification automatically cancels common terms in arithmetic 
1170 
expressions over nat and int; 

9542  1171 

10003  1172 
* ZF: new treatment of nat to minimize typechecking: all operators 
1173 
coerce their operands to a natural number using the function natify, 

1174 
making the algebraic laws unconditional; 

9542  1175 

10003  1176 
* ZF: as above, for int: operators coerce their operands to an integer 
1177 
using the function intify; 

9542  1178 

10003  1179 
* ZF: the integer library now contains many of the usual laws for the 
1180 
orderings, including $<=, and monotonicity laws for $+ and $*; 

9542  1181 

10003  1182 
* ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic 
1183 
simplification; 

9388  1184 

10003  1185 
* FOL and ZF: AddIffs now available, giving theorems of the form P<>Q 
1186 
to the simplifier and classical reasoner simultaneously; 

9388  1187 

1188 

8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

1189 
*** General *** 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

1190 

10003  1191 
* Provers: blast_tac now handles actual objectlogic rules as 
1192 
assumptions; note that auto_tac uses blast_tac internally as well; 

1193 

1194 
* Provers: new functions rulify/rulify_no_asm: thm > thm for turning 

1195 
outer >/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm; 

1196 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

1197 
* Provers: delrules now handles destruct rules as well (no longer need 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

1198 
explicit make_elim); 
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9937
diff
changeset

1199 

10003  1200 
* Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g. 
1201 
[ inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W ] ==> ?W 

1202 
use instead the strong form, 

1203 
[ inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W ] ==> ?W 

1204 
in HOL, FOL and ZF the function cla_make_elim will create such rules 

1205 
from destructrules; 

9489
aa757b35b129
* blast(_tac) now handles actual objectlogic rules as assumptions;
wenzelm
parents:
9457
diff
changeset

1206 

9709
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1207 
* Provers: Simplifier.easy_setup provides a fast path to basic 
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1208 
Simplifier setup for new objectlogics; 
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1209 

2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1210 
* Pure: AST translation rules no longer require constant head on LHS; 
9349
d43669fb423d
* tuned AST representation of nested pairs, avoiding bogus output in
wenzelm
parents:
9335
diff
changeset

1211 

9709
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1212 
* Pure: improved name spaces: ambiguous output is qualified; support 
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1213 
for hiding of names; 
8729
094dbd0fad0c
* improved name spaces: ambiguous output is qualified; support for
wenzelm
parents:
8705
diff
changeset

1214 

10003  1215 
* system: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and 
1216 
XSYMBOL_HOME; no longer need to do manual configuration in most 

1217 
situations; 

1218 

9709
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1219 
* system: compression of ML heaps images may now be controlled via c 
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1220 
option of isabelle and isatool usedir (currently only observed by 
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1221 
Poly/ML); 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

1222 

9981
01a0c4772c18
system: isatool installfonts may handle XSymbol fonts as well;
wenzelm
parents:
9971
diff
changeset

1223 
* system: isatool installfonts may handle XSymbol fonts as well (very 
01a0c4772c18
system: isatool installfonts may handle XSymbol fonts as well;
wenzelm
parents:
9971
diff
changeset

1224 
useful for remote X11); 
01a0c4772c18
system: isatool installfonts may handle XSymbol fonts as well;
wenzelm
parents:
9971
diff
changeset

1225 

9709
2d0ee9612ef1
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
wenzelm
parents:
9701
diff
changeset

1226 
* system: provide TAGS file for Isabelle sources; 
9052  1227 

9288
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9239
diff
changeset

1228 
* ML: infix 'OF' is a version of 'MRS' with more appropriate argument 
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9239
diff
changeset

1229 
order; 
06a55195741b
infix 'OF' is a version of 'MRS' with more appropriate argument order;
wenzelm
parents:
9239
diff
changeset

1230 

8994
803533fbb3ec
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
wenzelm
parents:
8991
diff
changeset

1231 
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global 
803533fbb3ec
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
wenzelm
parents:
8991
diff
changeset

1232 
timing flag supersedes proof_timing and Toplevel.trace; 
803533fbb3ec
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
wenzelm
parents:
8991
diff
changeset

1233 

10003  1234 
* ML: new combinators >> and >>> for incremental transformations 
1235 
with secondary results (e.g. certain theory extensions): 

1236 

9330
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

1237 
* ML: PureThy.add_defs gets additional argument to indicate potential 
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

1238 
overloading (usually false); 
6861e3b00155
HOL: the disjoint sum is now "<+>" instead of "Plus";
wenzelm
parents:
9288
diff
changeset

1239 

10003  1240 
* ML: PureThy.add_thms/add_axioms/add_defs now return theorems as 
1241 
results; 

8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

1242 

8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

1243 

8015  1244 

7986  1245 
New in Isabelle99 (October 1999) 
1246 
 

4649  1247 

5931  1248 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 
1249 

6922  1250 
* HOL: The THEN and ELSE parts of conditional expressions (if P then x else y) 
1251 
are no longer simplified. (This allows the simplifier to unfold recursive 

1252 
functional programs.) To restore the old behaviour, declare 

7215  1253 

1254 
Delcongs [if_weak_cong]; 

6922  1255 

6269  1256 
* HOL: Removed the obsolete syntax "Compl A"; use A for set 
1257 
complement; 

5931  1258 

6269  1259 
* HOL: the predicate "inj" is now defined by translation to "inj_on"; 
6174  1260 

7847  1261 
* HOL/datatype: mutual_induct_tac no longer exists  
1262 
use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"] 

1263 

6386
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

1264 
* HOL/typedef: fixed type inference for representing set; type 
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

1265 
arguments now have to occur explicitly on the rhs as type constraints; 
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

1266 

6269  1267 
* ZF: The con_defs part of an inductive definition may no longer refer 
1268 
to constants declared in the same theory; 

6057  1269 

6269  1270 
* HOL, ZF: the function mk_cases, generated by the inductive 
1271 
definition package, has lost an argument. To simplify its result, it 

1272 
uses the default simpset instead of a supplied list of theorems. 

6141  1273 

7215  1274 
* HOL/List: the constructors of type list are now Nil and Cons; 
1275 

7619  1276 
* Simplifier: the type of the infix ML functions 
8729
094dbd0fad0c
* improved name spaces: ambiguous output is qualified; support for
wenzelm
parents:
8705
diff
changeset

1277 
setSSolver addSSolver setSolver addSolver 
7619  1278 
is now simpset * solver > simpset where `solver' is a new abstract type 
1279 
for packaging solvers. A solver is created via 

8729
094dbd0fad0c
* improved name spaces: ambiguous output is qualified; support for
wenzelm
parents:
8705
diff
changeset

1280 
mk_solver: string > (thm list > int > tactic) > solver 
7619  1281 
where the string argument is only a comment. 
6057  1282 

7647
2ceddd91cd0a
proper handling of dangling sort hypotheses (at last!);
wenzelm
parents:
7619
diff
changeset

1283 

6069  1284 
*** Proof tools *** 
1285 

6343  1286 
* Provers/Arith/fast_lin_arith.ML contains a functor for creating a 
1287 
decision procedure for linear arithmetic. Currently it is used for 

7593  1288 
types `nat', `int', and `real' in HOL (see below); it can, should and 
1289 
will be instantiated for other types and logics as well. 

6069  1290 

7324  1291 
* The simplifier now accepts rewrite rules with flexible heads, eg 
1292 
hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y 

1293 
They are applied like any rule with a nonpattern lhs, i.e. by firstorder 

1294 
matching. 

6069  1295 

7593  1296 

6014  1297 
*** General *** 
1298 

7986  1299 
* New Isabelle/Isar subsystem provides an alternative to traditional 
7215  1300 
tactical theorem proving; together with the ProofGeneral/isar user 
1301 
interface it offers an interactive environment for developing human 

1302 
readable proof documents (Isar == Intelligible semiautomated 

7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

1303 
reasoning); for further information see isatool doc isarref, 
7986  1304 
src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/ 
7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

1305 

9612  1306 
* improved and simplified presentation of theories: better HTML markup 
1307 
(including colors), graph views in several sizes; isatool usedir now 

1308 
provides a proper interface for user theories (via P option); actual 

1309 
document preparation based on (PDF)LaTeX is available as well (for 

1310 
newstyle theories only); see isatool doc system for more information; 

7215  1311 

7252  1312 
* native support for Proof General, both for classic Isabelle and 
7986  1313 
Isabelle/Isar; 
7215  1314 

7791  1315 
* ML function thm_deps visualizes dependencies of theorems and lemmas, 
1316 
using the graph browser tool; 

1317 

6751  1318 
* Isabelle manuals now also available as PDF; 
1319 

6449  1320 
* theory loader rewritten from scratch (may not be fully 
1321 
bugcompatible); old loadpath variable has been replaced by show_path, 

6671  1322 
add_path, del_path, reset_path functions; new operations such as 
7593  1323 
update_thy, touch_thy, remove_thy, use/update_thy_only (see also 
1324 
isatool doc ref); 

6449  1325 

7215  1326 
* improved isatool install: option k creates KDE application icon, 
1327 
option p DIR installs standalone binaries; 

1328 

1329 
* added ML_PLATFORM setting (useful for crossplatform installations); 

1330 
more robust handling of platform specific ML images for SML/NJ; 

1331 

7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

1332 
* the settings environment is now statically scoped, i.e. it is never 
7986  1333 
created again in subprocesses invoked from isabelle, isatool, or 
7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

1334 
Isabelle; 
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

1335 

7215  1336 
* path element specification '~~' refers to '$ISABELLE_HOME'; 
1337 

6343  1338 
* in locales, the "assumes" and "defines" parts may be omitted if 
1339 
empty; 

5973  1340 

6269  1341 
* new print_mode "xsymbols" for extended symbol support (e.g. genuine 
1342 
long arrows); 

6259
488bdc1bd11a
path element specification '~~' refers to '$ISABELLE_HOME';
wenzelm
parents:
6174
diff
changeset

1343 

6343  1344 
* new print_mode "HTML"; 
1345 

1346 
* new flag show_tags controls display of tags of theorems (which are 

1347 
basically just comments that may be attached by some tools); 

1348 

6461  1349 
* Isamode 2.6 requires patch to accomodate change of Isabelle font 
1350 
mode and goal output format: 

1351 

1352 
diff r Isamode2.6/elisp/isaload.el Isamode/elisp/isaload.el 

1353 
244c244 

1354 
< (list (isagetenv "ISABELLE") "msymbols" logicname) 

1355 
 

6533  1356 
> (list (isagetenv "ISABELLE") "misabelle_font" "msymbols" logicname) 
6461  1357 
diff r Isabelle2.6/elisp/isaproofstate.el Isamode/elisp/isaproofstate.el 
1358 
181c181 

1359 
< (defconst proofstateproofstartregexp "^Level [09]+$" 

1360 
 

1361 
> (defconst proofstateproofstartregexp "^Level [09]+" 

1362 

7450  1363 
* function bind_thms stores lists of theorems (cf. bind_thm); 
1364 

7593  1365 
* new shorthand tactics ftac, eatac, datac, fatac; 
1366 

1367 
* qed (and friends) now accept "" as result name; in that case the 

7986  1368 
theorem is not stored, but proper checks and presentation of the 
1369 
result still apply; 

7593  1370 

7805
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7791
diff
changeset

1371 
* theorem database now also indexes constants "Trueprop", "all", 
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7791
diff
changeset

1372 
"==>", "=="; thus thms_containing, findI etc. may retrieve more rules; 
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7791
diff
changeset

1373 

6028  1374 

6057  1375 
*** HOL *** 
1376 

7215  1377 
** HOL arithmetic ** 
1378 

6343  1379 
* There are now decision procedures for linear arithmetic over nat and 
1380 
int: 

6131  1381 

6343  1382 
1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', 
1383 
`+', `', `Suc', `min', `max' and numerical constants; other subterms 

1384 
are treated as atomic; subformulae not involving type `nat' or `int' 

1385 
are ignored; quantified subformulae are ignored unless they are 

1386 
positive universal or negative existential. The tactic has to be 

1387 
invoked by hand and can be a little bit slow. In particular, the 

1388 
running time is exponential in the number of occurrences of `min' and 

1389 
`max', and `' on `nat'. 

6131  1390 

6343  1391 
2. fast_arith_tac is a cutdown version of arith_tac: it only takes 
1392 
(negated) (in)equalities among the premises and the conclusion into 

1393 
account (i.e. no compound formulae) and does not know about `min' and 

1394 
`max', and `' on `nat'. It is fast and is used automatically by the 

1395 
simplifier. 

6131  1396 

6343  1397 
NB: At the moment, these decision procedures do not cope with mixed 
1398 
nat/int formulae where the two parts interact, such as `m < n ==> 

1399 
int(m) < int(n)'. 

6028  1400 

7215  1401 
* HOL/Numeral provides a generic theory of numerals (encoded 
7313  1402 
efficiently as bit strings); setup for types nat/int/real is in place; 
7215  1403 
INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than 
1404 
int, existing theories and proof scripts may require a few additional 

1405 
type constraints; 

1406 

1407 
* integer division and remainder can now be performed on constant 

1408 
arguments; 

7157  1409 

7215  1410 
* many properties of integer multiplication, division and remainder 
1411 
are now available; 

6922  1412 

7287  1413 
* An interface to the Stanford Validity Checker (SVC) is available through the 
1414 
tactic svc_tac. Propositional tautologies and theorems of linear arithmetic 

d603a06b30df
defer_recdef
pau& 