author  obua 
Tue, 13 Sep 2005 17:05:59 +0200  
changeset 17335  7cff05c90a0e 
parent 17275  44d8fbc2e52d 
child 17371  923ef4a8c672 
permissions  rwrr 
5363  1 
Isabelle NEWS  history userrelevant changes 
2 
============================================== 

2553  3 

14655
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

4 
New in this Isabelle release 
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

5 
 
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

6 

8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

7 
*** General *** 
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

8 

15130  9 
* Theory headers: the new header syntax for Isar theories is 
10 

11 
theory <name> 

16234  12 
imports <theory1> ... <theoryN> 
13 
uses <file1> ... <fileM> 

15130  14 
begin 
15 

16234  16 
where the 'uses' part is optional. The previous syntax 
17 

18 
theory <name> = <theory1> + ... + <theoryN>: 

19 

16717  20 
will disappear in the next release. Use isatool fixheaders to convert 
21 
existing theory files. Note that there is no change in ancient 

17189  22 
nonIsar theories now, but these are likely to disappear soon. 
15130  23 

15475
fdf9434b04ea
 Proofs are now hidden by default when generating documents
berghofe
parents:
15454
diff
changeset

24 
* Theory loader: parent theories can now also be referred to via 
16234  25 
relative and absolute paths. 
26 

27 
* Improved version of thms_containing searches for a list of criteria 

28 
instead of a list of constants. Known criteria are: intro, elim, dest, 

29 
name:string, simp:term, and any term. Criteria can be preceded by '' 

30 
to select theorems that do not match. Intro, elim, dest select 

31 
theorems that match the current goal, name:s selects theorems whose 

32 
fully qualified name contain s, and simp:term selects all 

33 
simplification rules whose lhs match term. Any other term is 

34 
interpreted as pattern and selects all theorems matching the 

35 
pattern. Available in ProofGeneral under 'ProofGeneral > Find 

36 
Theorems' or Cc Cf. Example: 

37 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

38 
Cc Cf (100) "(_::nat) + _ + _" intro name: "HOL." 
16234  39 

40 
prints the last 100 theorems matching the pattern "(_::nat) + _ + _", 

41 
matching the current goal as introduction rule and not having "HOL." 

42 
in their name (i.e. not being defined in theory HOL). 

16013
3010430d894d
removed find_rewrites (superceded by improved thms_containing);
wenzelm
parents:
16000
diff
changeset

43 

15703  44 

45 
*** Document preparation *** 

46 

16234  47 
* Commands 'display_drafts' and 'print_drafts' perform simple output 
48 
of raw sources. Only those symbols that do not require additional 

49 
LaTeX packages (depending on comments in isabellesym.sty) are 

50 
displayed properly, everything else is left verbatim. isatool display 

51 
and isatool print are used as front ends (these are subject to the 

52 
DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively). 

53 

17047
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

54 
* Command tags control specific markup of certain regions of text, 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

55 
notably folding and hiding. Predefined tags include "theory" (for 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

56 
theory begin and end), "proof" for proof commands, and "ML" for 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

57 
commands involving ML code; the additional tags "visible" and 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

58 
"invisible" are unused by default. Users may give explicit tag 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

59 
specifications in the text, e.g. ''by %invisible (auto)''. The 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

60 
interpretation of tags is determined by the LaTeX job during document 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

61 
preparation: see option V of isatool usedir, or options n and t of 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

62 
isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag, 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

63 
\isadroptag. 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

64 

e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

65 
Several document versions may be produced at the same time via isatool 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

66 
usedir (the generated index.html will link all of them). Typical 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

67 
specifications include ''V document=theory,proof,ML'' to present 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

68 
theory/proof/ML parts faithfully, ''V outline=/proof,/ML'' to fold 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

69 
proof and ML commands, and ''V mutilated=theory,proof,ML'' to omit 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

70 
these parts without any formal replacement text. The Isabelle site 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

71 
default settings produce ''document'' and ''outline'' versions as 
e2e2d75bb37b
* Command tags control specific markup of certain regions of text (replaces usedir H);
wenzelm
parents:
17016
diff
changeset

72 
specified above. 
16234  73 

15979  74 
* Several new antiquotation: 
75 

76 
@{term_type term} prints a term with its type annotated; 

77 

78 
@{typeof term} prints the type of a term; 

79 

16234  80 
@{const const} is the same as @{term const}, but checks that the 
81 
argument is a known logical constant; 

15979  82 

83 
@{term_style style term} and @{thm_style style thm} print a term or 

16234  84 
theorem applying a "style" to it 
85 

17117
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

86 
@{ML text} 
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

87 

16234  88 
Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of 
89 
definitions, equations, inequations etc., 'concl' printing only the 

90 
conclusion of a metalogical statement theorem, and 'prem1' .. 'prem9' 

91 
to print the specified premise. TermStyle.add_style provides an ML 

92 
interface for introducing further styles. See also the "LaTeX Sugar" 

17117
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

93 
document practical applications. The ML antiquotation prints 
e2bed9e82454
* The ML antiquotation prints typechecked ML expressions verbatim.
wenzelm
parents:
17097
diff
changeset

94 
typechecked ML expressions verbatim. 
16234  95 

17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

96 
* Markup commands 'chapter', 'section', 'subsection', 'subsubsection', 
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

97 
and 'text' support optional locale specification '(in loc)', which 
17269  98 
specifies the default context for interpreting antiquotations. For 
99 
example: 'text (in lattice) {* @{thm inf_assoc}*}'. 

17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

100 

dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

101 
* Option 'locale=NAME' of antiquotations specifies an alternative 
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

102 
context interpreting the subsequent argument. For example: @{thm 
17269  103 
[locale=lattice] inf_assoc}. 
17259
dda237f1d299
Markup commands 'chapter' .. 'text' support optional locale specification;
wenzelm
parents:
17228
diff
changeset

104 

17097
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

105 
* Proper output of proof terms (@{prf ...} and @{full_prf ...}) within 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

106 
a proof context. 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

107 

78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

108 
* Proper output of antiquotations for theory commands involving a 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

109 
proof context (such as 'locale' or 'theorem (in loc) ...'). 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

110 

17193
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

111 
* Delimiters of outer tokens (string etc.) now produce separate LaTeX 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

112 
macros (\isachardoublequoteopen, isachardoublequoteclose etc.). 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

113 

83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

114 
* isatool usedir: new option C (default true) controls whether option 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

115 
D should include a copy of the original document directory; C false 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

116 
prevents unwanted effects such as copying of administrative CVS data. 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

117 

16234  118 

119 
*** Pure *** 

120 

121 
* Considerably improved version of 'constdefs' command. Now performs 

122 
automatic typeinference of declared constants; additional support for 

123 
local structure declarations (cf. locales and HOL records), see also 

124 
isarref manual. Potential INCOMPATIBILITY: need to observe strictly 

125 
sequential dependencies of definitions within a single 'constdefs' 

126 
section; moreover, the declared name needs to be an identifier. If 

127 
all fails, consider to fall back on 'consts' and 'defs' separately. 

128 

129 
* Improved indexed syntax and implicit structures. First of all, 

130 
indexed syntax provides a notational device for subscripted 

131 
application, using the new syntax \<^bsub>term\<^esub> for arbitrary 

132 
expressions. Secondly, in a local context with structure 

133 
declarations, number indexes \<^sub>n or the empty index (default 

134 
number 1) refer to a certain fixed variable implicitly; option 

135 
show_structs controls printing of implicit structures. Typical 

136 
applications of these concepts involve record types and locales. 

137 

138 
* New command 'no_syntax' removes grammar declarations (and 

139 
translations) resulting from the given syntax specification, which is 

140 
interpreted in the same manner as for the 'syntax' command. 

141 

142 
* 'Advanced' translation functions (parse_translation etc.) may depend 

143 
on the signature of the theory context being presently used for 

144 
parsing/printing, see also isarref manual. 

145 

16856  146 
* Improved 'oracle' command provides a typesafe interface to turn an 
147 
ML expression of type theory > T > term into a primitive rule of 

148 
type theory > T > thm (i.e. the functionality of Thm.invoke_oracle 

149 
is already included here); see also FOL/ex/IffExample.thy; 

150 
INCOMPATIBILITY. 

151 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

152 
* axclass: name space prefix for class "c" is now "c_class" (was "c" 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

153 
before); "cI" is no longer bound, use "c.intro" instead. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

154 
INCOMPATIBILITY. This change avoids clashes of fact bindings for 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

155 
axclasses vs. locales. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

156 

16234  157 
* Improved internal renaming of symbolic identifiers  attach primes 
158 
instead of base 26 numbers. 

159 

160 
* New flag show_question_marks controls printing of leading question 

161 
marks in schematic variable names. 

162 

163 
* In schematic variable names, *any* symbol following \<^isub> or 

164 
\<^isup> is now treated as part of the base name. For example, the 

165 
following works without printing of awkward ".0" indexes: 

166 

167 
lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" 

168 
by simp 

169 

170 
* Inner syntax includes (*(*nested*) comments*). 

171 

172 
* Pretty pinter now supports unbreakable blocks, specified in mixfix 

173 
annotations as "(00...)". 

174 

175 
* Clear separation of logical types and nonterminals, where the latter 

176 
may only occur in 'syntax' specifications or type abbreviations. 

177 
Before that distinction was only partially implemented via type class 

178 
"logic" vs. "{}". Potential INCOMPATIBILITY in rare cases of improper 

179 
use of 'types'/'consts' instead of 'nonterminals'/'syntax'. Some very 

180 
exotic syntax specifications may require further adaption 

181 
(e.g. Cube/Base.thy). 

182 

183 
* Removed obsolete type class "logic", use the top sort {} instead. 

184 
Note that nonlogical types should be declared as 'nonterminals' 

185 
rather than 'types'. INCOMPATIBILITY for new objectlogic 

186 
specifications. 

187 

17095  188 
* Attributes 'induct' and 'cases': type or set names may now be 
189 
locally fixed variables as well. 

190 

16234  191 
* Simplifier: can now control the depth to which conditional rewriting 
192 
is traced via the PG menu Isabelle > Settings > Trace Simp Depth 

193 
Limit. 

194 

195 
* Simplifier: simplification procedures may now take the current 

196 
simpset into account (cf. Simplifier.simproc(_i) / mk_simproc 

197 
interface), which is very useful for calling the Simplifier 

198 
recursively. Minor INCOMPATIBILITY: the 'prems' argument of simprocs 

199 
is gone  use prems_of_ss on the simpset instead. Moreover, the 

200 
lowlevel mk_simproc no longer applies Logic.varify internally, to 

201 
allow for use in a context of fixed variables. 

202 

203 
* thin_tac now works even if the assumption being deleted contains !! 

204 
or ==>. More generally, erule now works even if the major premise of 

205 
the elimination rule contains !! or ==>. 

206 

207 
* Reorganized bootstrapping of the Pure theories; CPure is now derived 

208 
from Pure, which contains all common declarations already. Both 

209 
theories are defined via plain Isabelle/Isar .thy files. 

210 
INCOMPATIBILITY: elements of CPure (such as the CPure.intro / 

211 
CPure.elim / CPure.dest attributes) now appear in the Pure name space; 

212 
use isatool fixcpure to adapt your theory and ML sources. 

213 

214 
* New syntax 'name(ij, i, i, ...)' for referring to specific 

215 
selections of theorems in named facts via index ranges. 

216 

17097
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

217 
* 'print_theorems': in theory mode, really print the difference 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

218 
wrt. the last state (works for interactive theory development only), 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

219 
in proof mode print all local facts (cf. 'print_facts'); 
78f1b66f70a4
* Proper output of proof terms within a proof context;
wenzelm
parents:
17095
diff
changeset

220 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

221 
* More efficient treatment of intermediate checkpoints in interactive 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

222 
theory development. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

223 

16234  224 

225 
*** Locales *** 

17095  226 

227 
* New commands for the interpretation of locale expressions in theories (1), 

228 
locales (2) and proof contexts (3). These generate proof obligations from 

229 
the expression specification. After the obligations have been discharged, 

230 
theorems of the expression are added to the theory, target locale or proof 

231 
context. The synopsis of the commands is a follows: 

232 
(1) interpretation expr inst 

233 
(2) interpretation target < expr 

234 
(3) interpret expr inst 

235 
Interpretation in theories and proof contexts require a parameter 

236 
instantiation of terms from the current context. This is applied to 

237 
specifications and theorems of the interpreted expression. Interpretation 

238 
in locales only permits parameter renaming through the locale expression. 

17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17117
diff
changeset

239 
Interpretation is smart in that interpretations that are active already 
17095  240 
do not occur in proof obligations, neither are instantiated theorems stored 
241 
in duplicate. Use 'print_interps' to inspect active interpretations of 

242 
a particular locale. For details, see the Isar Reference manual. 

16234  243 

244 
INCOMPATIBILITY: former 'instantiate' has been withdrawn, use 

245 
'interpret' instead. 

246 

17095  247 
* New context element 'constrains' for adding type constraints to parameters. 
248 

249 
* Context expressions: renaming of parameters with syntax redeclaration. 

250 

251 
* Locale declaration: 'includes' disallowed. 

252 

16234  253 
* Proper static binding of attribute syntax  i.e. types / terms / 
254 
facts mentioned as arguments are always those of the locale definition 

255 
context, independently of the context of later invocations. Moreover, 

256 
locale operations (renaming and type / term instantiation) are applied 

257 
to attribute arguments as expected. 

258 

259 
INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of 

260 
actual attributes; rare situations may require Attrib.attribute to 

261 
embed those attributes into Attrib.src that lack concrete syntax. 

262 
Attribute implementations need to cooperate properly with the static 

263 
binding mechanism. Basic parsers Args.XXX_typ/term/prop and 

264 
Attrib.XXX_thm etc. already do the right thing without further 

265 
intervention. Only unusual applications  such as "where" or "of" 

266 
(cf. src/Pure/Isar/attrib.ML), which process arguments depending both 

267 
on the context and the facts involved  may have to assign parsed 

268 
values to argument tokens explicitly. 

269 

270 
* Changed parameter management in theorem generation for long goal 

271 
statements with 'includes'. INCOMPATIBILITY: produces a different 

272 
theorem statement in rare situations. 

273 

17228  274 
* Locale inspection command 'print_locale' omits notes elements. Use 
275 
'print_locale!' to have them included in the output. 

276 

16234  277 

278 
*** Provers *** 

279 

280 
* Provers/hypsubst.ML: improved version of the subst method, for 

281 
singlestep rewriting: it now works in bound variable contexts. New is 

282 
'subst (asm)', for rewriting an assumption. INCOMPATIBILITY: may 

283 
rewrite a different subterm than the original subst method, which is 

284 
still available as 'simplesubst'. 

285 

286 
* Provers/quasi.ML: new transitivity reasoners for transitivity only 

287 
and quasi orders. 

288 

289 
* Provers/trancl.ML: new transitivity reasoner for transitive and 

290 
reflexivetransitive closure of relations. 

291 

292 
* Provers/blast.ML: new reference depth_limit to make blast's depth 

293 
limit (previously hardcoded with a value of 20) userdefinable. 

294 

295 
* Provers/simplifier.ML has been moved to Pure, where Simplifier.setup 

296 
is peformed already. Objectlogics merely need to finish their 

297 
initial simpset configuration as before. INCOMPATIBILITY. 

15703  298 

15475
fdf9434b04ea
 Proofs are now hidden by default when generating documents
berghofe
parents:
15454
diff
changeset

299 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14699
diff
changeset

300 
*** HOL *** 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14699
diff
changeset

301 

16234  302 
* Symbolic syntax of Hilbert Choice Operator is now as follows: 
14878  303 

304 
syntax (epsilon) 

305 
"_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) 

306 

16234  307 
The symbol \<some> is displayed as the alternative epsilon of LaTeX 
308 
and xsymbol; use option 'm epsilon' to get it actually printed. 

309 
Moreover, the mathematically important symbolic identifier \<epsilon> 

310 
becomes available as variable, constant etc. INCOMPATIBILITY, 

311 

312 
* "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x". 

313 
Similarly for all quantifiers: "ALL x > y" etc. The xsymbol for >= 

17016
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

314 
is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to 
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

315 
support corresponding Isar calculations. 
16234  316 

317 
* "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>" 

318 
instead of ":". 

319 

320 
* theory SetInterval: changed the syntax for open intervals: 

321 

322 
Old New 

323 
{..n(} {..<n} 

324 
{)n..} {n<..} 

325 
{m..n(} {m..<n} 

326 
{)m..n} {m<..n} 

327 
{)m..n(} {m<..<n} 

328 

329 
The old syntax is still supported but will disappear in the next 

330 
release. For conversion use the following Emacs search and replace 

331 
patterns (these are not perfect but work quite well): 

15046  332 

333 
{)\([^\.]*\)\.\. > {\1<\.\.} 

334 
\.\.\([^(}]*\)(} > \.\.<\1} 

335 

16234  336 
* theory Finite_Set: changed the syntax for 'setsum', summation over 
337 
finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is 

17189  338 
now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can 
339 
be a tuple pattern. 

16234  340 

341 
Some new syntax forms are available: 

342 

343 
"\<Sum>x  P. e" for "setsum (%x. e) {x. P}" 

344 
"\<Sum>x = a..b. e" for "setsum (%x. e) {a..b}" 

345 
"\<Sum>x = a..<b. e" for "setsum (%x. e) {a..<b}" 

346 
"\<Sum>x < k. e" for "setsum (%x. e) {..<k}" 

347 

348 
The latter form "\<Sum>x < k. e" used to be based on a separate 

349 
function "Summation", which has been discontinued. 

350 

351 
* theory Finite_Set: in structured induction proofs, the insert case 

352 
is now 'case (insert x F)' instead of the old counterintuitive 'case 

353 
(insert F x)'. 

354 

355 
* The 'refute' command has been extended to support a much larger 

356 
fragment of HOL, including axiomatic type classes, constdefs and 

357 
typedefs, inductive datatypes and recursion. 

358 

359 
* Datatype induction via method 'induct' now preserves the name of the 

360 
induction variable. For example, when proving P(xs::'a list) by 

361 
induction on xs, the induction step is now P(xs) ==> P(a#xs) rather 

362 
than P(list) ==> P(a#list) as previously. Potential INCOMPATIBILITY 

363 
in unstructured proof scripts. 

364 

365 
* Reworked implementation of records. Improved scalability for 

366 
records with many fields, avoiding performance problems for type 

367 
inference. Records are no longer composed of nested field types, but 

368 
of nested extension types. Therefore the record type only grows linear 

369 
in the number of extensions and not in the number of fields. The 

370 
toplevel (users) view on records is preserved. Potential 

371 
INCOMPATIBILITY only in strange cases, where the theory depends on the 

372 
old record representation. The type generated for a record is called 

373 
<record_name>_ext_type. 

374 

375 
Flag record_quick_and_dirty_sensitive can be enabled to skip the 

376 
proofs triggered by a record definition or a simproc (if 

377 
quick_and_dirty is enabled). Definitions of large records can take 

378 
quite long. 

379 

380 
New simproc record_upd_simproc for simplification of multiple record 

381 
updates enabled by default. Moreover, trivial updates are also 

382 
removed: r(x := x r) = r. INCOMPATIBILITY: old proofs break 

383 
occasionally, since simplification is more powerful by default. 

384 

17275
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

385 
* typedef: proper support for polymorphic sets, which contain extra 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

386 
typevariables in the term. 
44d8fbc2e52d
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17269
diff
changeset

387 

16234  388 
* Simplifier: automatically reasons about transitivity chains 
389 
involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics 

390 
provided by Provers/trancl.ML as additional solvers. INCOMPATIBILITY: 

391 
old proofs break occasionally as simplification may now solve more 

392 
goals than previously. 

393 

394 
* Simplifier: converts x <= y into x = y if assumption y <= x is 

395 
present. Works for all partial orders (class "order"), in particular 

396 
numbers and sets. For linear orders (e.g. numbers) it treats ~ x < y 

397 
just like y <= x. 

398 

399 
* Simplifier: new simproc for "let x = a in f x". If a is a free or 

400 
bound variable or a constant then the let is unfolded. Otherwise 

401 
first a is simplified to b, and then f b is simplified to g. If 

402 
possible we abstract b from g arriving at "let x = b in h x", 

403 
otherwise we unfold the let and arrive at g. The simproc can be 

404 
enabled/disabled by the reference use_let_simproc. Potential 

405 
INCOMPATIBILITY since simplification is more powerful by default. 

15776  406 

16563  407 
* Classical reasoning: the meson method now accepts theorems as arguments. 
408 

16891  409 
* Theory OrderedGroup and Ring_and_Field: various additions and 
410 
improvements to faciliate calculations involving equalities and 

411 
inequalities. 

412 

413 
The following theorems have been eliminated or modified 

414 
(INCOMPATIBILITY): 

16888  415 

416 
abs_eq now named abs_of_nonneg 

417 
abs_of_ge_0 now named abs_of_nonneg 

418 
abs_minus_eq now named abs_of_nonpos 

419 
imp_abs_id now named abs_of_nonneg 

420 
imp_abs_neg_id now named abs_of_nonpos 

421 
mult_pos now named mult_pos_pos 

422 
mult_pos_le now named mult_nonneg_nonneg 

423 
mult_pos_neg_le now named mult_nonneg_nonpos 

424 
mult_pos_neg2_le now named mult_nonneg_nonpos2 

425 
mult_neg now named mult_neg_neg 

426 
mult_neg_le now named mult_nonpos_nonpos 

427 

16891  428 
* Theory Parity: added rules for simplifying exponents. 
429 

17092  430 
* Theory List: 
431 

432 
The following theorems have been eliminated or modified 

433 
(INCOMPATIBILITY): 

434 

435 
list_all_Nil now named list_all.simps(1) 

436 
list_all_Cons now named list_all.simps(2) 

437 
list_all_conv now named list_all_iff 

438 
set_mem_eq now named mem_iff 

439 

16929  440 
* Theories SetsAndFunctions and BigO (see HOL/Library) support 
441 
asymptotic "big O" calculations. See the notes in BigO.thy. 

442 

16888  443 

444 
*** HOLComplex *** 

445 

16891  446 
* Theory RealDef: better support for embedding natural numbers and 
447 
integers in the reals. 

448 

449 
The following theorems have been eliminated or modified 

450 
(INCOMPATIBILITY): 

451 

17016
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

452 
exp_ge_add_one_self now requires no hypotheses 
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

453 
real_of_int_add reversed direction of equality (use [symmetric]) 
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

454 
real_of_int_minus reversed direction of equality (use [symmetric]) 
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

455 
real_of_int_diff reversed direction of equality (use [symmetric]) 
73c74cb1d744
mentioned change to exp_ge_add_one_self, new transitivity rules
avigad
parents:
16997
diff
changeset

456 
real_of_int_mult reversed direction of equality (use [symmetric]) 
16891  457 

458 
* Theory RComplete: expanded support for floor and ceiling functions. 

16888  459 

16962  460 
* Theory Ln is new, with properties of the natural logarithm 
461 

14655
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

462 

14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset

463 
*** HOLCF *** 
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset

464 

a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset

465 
* HOLCF: discontinued special version of 'constdefs' (which used to 
16234  466 
support continuous functions) in favor of the general Pure one with 
467 
full typeinference. 

14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset

468 

a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14655
diff
changeset

469 

14885  470 
*** ZF *** 
471 

16234  472 
* ZF/ex: theories Group and Ring provide examples in abstract algebra, 
473 
including the First Isomorphism Theorem (on quotienting by the kernel 

474 
of a homomorphism). 

15089
430264838064
ZF/Simplifier: second copy of context type solver;
wenzelm
parents:
15076
diff
changeset

475 

430264838064
ZF/Simplifier: second copy of context type solver;
wenzelm
parents:
15076
diff
changeset

476 
* ZF/Simplifier: install second copy of type solver that actually 
16234  477 
makes use of TC rules declared to Isar proof contexts (or locales); 
478 
the old version is still required for ML proof scripts. 

15703  479 

480 

481 
*** ML *** 

482 

15973  483 
* Pure/library.ML no longer defines its own option datatype, but uses 
16234  484 
that of the SML basis, which has constructors NONE and SOME instead of 
485 
None and Some, as well as exception Option.Option instead of OPTION. 

486 
The functions the, if_none, is_some, is_none have been adapted 

487 
accordingly, while Option.map replaces apsome. 

15973  488 

16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

489 
* Pure/library.ML: the exception LIST has been given up in favour of 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

490 
the standard exceptions Empty and Subscript, as well as 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

491 
Library.UnequalLengths. Function like Library.hd and Library.tl are 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

492 
superceded by the standard hd and tl functions etc. 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

493 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

494 
A number of basic list functions are no longer exported to the ML 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

495 
toplevel, as they are variants of predefined functions. The following 
16234  496 
suggests how one can translate existing code: 
15973  497 

498 
rev_append xs ys = List.revAppend (xs, ys) 

499 
nth_elem (i, xs) = List.nth (xs, i) 

500 
last_elem xs = List.last xs 

501 
flat xss = List.concat xss 

16234  502 
seq fs = List.app fs 
15973  503 
partition P xs = List.partition P xs 
504 
mapfilter f xs = List.mapPartial f xs 

505 

16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

506 
* Pure/library.ML: several combinators for linear functional 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

507 
transformations, notably reverse application and composition: 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

508 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

509 
x > f f #> g 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

510 
(x, y) > f f #> g 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

511 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

512 
* Pure/library.ML: canonical list combinators fold, fold_rev, and 
16869  513 
fold_map support linear functional transformations and nesting. For 
16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

514 
example: 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

515 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

516 
fold f [x1, ..., xN] y = 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

517 
y > f x1 > ... > f xN 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

518 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

519 
(fold o fold) f [xs1, ..., xsN] y = 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

520 
y > fold f xs1 > ... > fold f xsN 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

521 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

522 
fold f [x1, ..., xN] = 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

523 
f x1 #> ... #> f xN 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

524 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

525 
(fold o fold) f [xs1, ..., xsN] = 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

526 
fold f xs1 #> ... #> fold f xsN 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

527 

43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

528 
* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

529 
fold_types traverse types/terms from left to right, observing 
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

530 
canonical argument order. Supercedes previous foldl_XXX versions, 
16868  531 
add_frees, add_vars etc. have been adapted as well: INCOMPATIBILITY. 
16860
43abdba4da5c
* Pure/library.ML: several combinators for linear functional transformations;
wenzelm
parents:
16856
diff
changeset

532 

15703  533 
* Pure: output via the Isabelle channels of writeln/warning/error 
16234  534 
etc. is now passed through Output.output, with a hook for arbitrary 
535 
transformations depending on the print_mode (cf. Output.add_mode  

536 
the first active mode that provides a output function wins). Already 

537 
formatted output may be embedded into further text via Output.raw; the 

538 
result of Pretty.string_of/str_of and derived functions 

539 
(string_of_term/cterm/thm etc.) is already marked raw to accommodate 

540 
easy composition of diagnostic messages etc. Programmers rarely need 

541 
to care about Output.output or Output.raw at all, with some notable 

542 
exceptions: Output.output is required when bypassing the standard 

543 
channels (writeln etc.), or in token translations to produce properly 

544 
formatted results; Output.raw is required when capturing already 

545 
output material that will eventually be presented to the user a second 

546 
time. For the default print mode, both Output.output and Output.raw 

547 
have no effect. 

548 

16718  549 
* Pure: Output.time_accumulator NAME creates an operator ('a > 'b) > 
550 
'a > 'b to measure runtime and count invocations; the cumulative 

551 
results are displayed at the end of a batch session. 

552 

553 
* Isar toplevel: improved diagnostics, mostly for Poly/ML only. 

554 
Reference Toplevel.debug (default false) controls detailed printing 

555 
and tracing of lowlevel exceptions; Toplevel.profiling (default 0) 

556 
controls execution profiling  set to 1 for time and 2 for space 

557 
(both increase the runtime). 

15703  558 

16799
978dcf30c3dd
* Isar session: The initial use of ROOT.ML is now always timed;
wenzelm
parents:
16718
diff
changeset

559 
* Isar session: The initial use of ROOT.ML is now always timed, 
978dcf30c3dd
* Isar session: The initial use of ROOT.ML is now always timed;
wenzelm
parents:
16718
diff
changeset

560 
i.e. the log will show the actual process times, in contrast to the 
978dcf30c3dd
* Isar session: The initial use of ROOT.ML is now always timed;
wenzelm
parents:
16718
diff
changeset

561 
elapsed wallclock time that the outer shell wrapper produces. 
978dcf30c3dd
* Isar session: The initial use of ROOT.ML is now always timed;
wenzelm
parents:
16718
diff
changeset

562 

16689
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

563 
* Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a 
16690  564 
reasonably efficient lightweight implementation of sets as lists. 
16689
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

565 

05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

566 
* Pure: more efficient orders for basic syntactic entities: added 
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

567 
fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord 
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

568 
and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is 
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

569 
NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast 
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

570 
orders now  potential INCOMPATIBILITY for code that depends on a 
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

571 
particular order for Symtab.keys, Symtab.dest, etc. (consider using 
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

572 
Library.sort_strings on result). 
05b986733a59
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
wenzelm
parents:
16662
diff
changeset

573 

16151  574 
* Pure: name spaces have been refined, with significant changes of the 
16234  575 
internal interfaces  INCOMPATIBILITY. Renamed cond_extern(_table) 
576 
to extern(_table). The plain name entry path is superceded by a 

577 
general 'naming' context, which also includes the 'policy' to produce 

578 
a fully qualified name and external accesses of a fully qualified 

579 
name; NameSpace.extend is superceded by context dependent 

580 
Sign.declare_name. Several theory and proof context operations modify 

581 
the naming context. Especially note Theory.restore_naming and 

582 
ProofContext.restore_naming to get back to a sane state; note that 

583 
Theory.add_path is no longer sufficient to recover from 

584 
Theory.absolute_path in particular. 

585 

586 
* Pure: new flags short_names (default false) and unique_names 

587 
(default true) for controlling output of qualified names. If 

588 
short_names is set, names are printed unqualified. If unique_names is 

589 
reset, the name prefix is reduced to the minimum required to achieve 

590 
the original result when interning again, even if there is an overlap 

591 
with earlier declarations. 

16151  592 

16456
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

593 
* Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

594 
now 'extend', and 'merge' gets an additional Pretty.pp argument 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

595 
(useful for printing error messages). INCOMPATIBILITY. 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

596 

451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

597 
* Pure: major reorganization of the theory context. Type Sign.sg and 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

598 
Theory.theory are now identified, referring to the universal 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

599 
Context.theory (see Pure/context.ML). Actual signature and theory 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

600 
content is managed as theory data. The old code and interfaces were 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

601 
spread over many files and structures; the new arrangement introduces 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

602 
considerable INCOMPATIBILITY to gain more clarity: 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

603 

451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

604 
Context  theory management operations (name, identity, inclusion, 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

605 
parents, ancestors, merge, etc.), plus generic theory data; 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

606 

451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

607 
Sign  logical signature and syntax operations (declaring consts, 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

608 
types, etc.), plus certify/read for common entities; 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

609 

451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

610 
Theory  logical theory operations (stating axioms, definitions, 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

611 
oracles), plus a copy of logical signature operations (consts, 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

612 
types, etc.); also a few basic management operations (Theory.copy, 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

613 
Theory.merge, etc.) 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

614 

451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

615 
The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

616 
etc.) as well as the sign field in Thm.rep_thm etc. have been retained 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

617 
for convenience  they merely return the theory. 
451f1c46d4ca
* Pure/TheoryDataFun: change of the argument structure;
wenzelm
parents:
16373
diff
changeset

618 

17193
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

619 
* Pure: type Type.tsig is superceded by theory in most interfaces. 
83708f724822
* Delimiters of outer tokens now produce separate LaTeX macros;
wenzelm
parents:
17189
diff
changeset

620 

16547
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset

621 
* Pure: the Isar proof context type is already defined early in Pure 
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset

622 
as Context.proof (note that ProofContext.context and Proof.context are 
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset

623 
aliases, where the latter is the preferred name). This enables other 
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset

624 
Isabelle components to refer to that type even before Isar is present. 
09f7a953d2d6
* Pure: the Isar proof context type is already defined early in Pure
wenzelm
parents:
16506
diff
changeset

625 

16373
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

626 
* Pure/sign/theory: discontinued named name spaces (i.e. classK, 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

627 
typeK, constK, axiomK, oracleK), but provide explicit operations for 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

628 
any of these kinds. For example, Sign.intern typeK is now 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

629 
Sign.intern_type, Theory.hide_space Sign.typeK is now 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

630 
Theory.hide_types. Also note that former 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

631 
Theory.hide_classes/types/consts are now 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

632 
Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

633 
internalize their arguments! INCOMPATIBILITY. 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

634 

16506
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset

635 
* Pure: get_thm interface (of PureThy and ProofContext) expects 
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset

636 
datatype thmref (with constructors Name and NameSelection) instead of 
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset

637 
plain string  INCOMPATIBILITY; 
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset

638 

16151  639 
* Pure: cases produced by proof methods specify options, where NONE 
16234  640 
means to remove case bindings  INCOMPATIBILITY in 
641 
(RAW_)METHOD_CASES. 

16151  642 

16373
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

643 
* Pure: the following operations retrieve axioms or theorems from a 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

644 
theory node or theory hierarchy, respectively: 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

645 

9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

646 
Theory.axioms_of: theory > (string * term) list 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

647 
Theory.all_axioms_of: theory > (string * term) list 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

648 
PureThy.thms_of: theory > (string * thm) list 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

649 
PureThy.all_thms_of: theory > (string * thm) list 
9d020423093b
* Pure/sign/theory: discontinued named name spaces;
wenzelm
parents:
16251
diff
changeset

650 

16718  651 
* Pure: print_tac now outputs the goal through the trace channel. 
652 

16997
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

653 
* Pure/Simplifier: improved handling of bound variables (nameless 
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

654 
representation, avoid allocating new strings). Simprocs that invoke 
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

655 
the Simplifier recursively should use Simplifier.inherit_bounds to 
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

656 
avoid local name clashes. 
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

657 

7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

658 
* Pure/Provers: Simplifier and Classical Reasoner now support proof 
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

659 
context dependent plugins (simprocs, solvers, wrappers etc.). These 
7dfc99f62dd9
* Pure/Simplifier: improved handling of bound variables;
wenzelm
parents:
16962
diff
changeset

660 
extra components are stored in the theory and patched into the 
16234  661 
simpset/claset when used in an Isar proof context. Context dependent 
662 
components are maintained by the following theory operations: 

663 

664 
Simplifier.add_context_simprocs 

665 
Simplifier.del_context_simprocs 

666 
Simplifier.set_context_subgoaler 

667 
Simplifier.reset_context_subgoaler 

668 
Simplifier.add_context_looper 

669 
Simplifier.del_context_looper 

670 
Simplifier.add_context_unsafe_solver 

671 
Simplifier.add_context_safe_solver 

672 

673 
Classical.add_context_safe_wrapper 

674 
Classical.del_context_safe_wrapper 

675 
Classical.add_context_unsafe_wrapper 

676 
Classical.del_context_unsafe_wrapper 

677 

678 
IMPORTANT NOTE: proof tools (methods etc.) need to use 

679 
local_simpset_of and local_claset_of to instead of the primitive 

680 
Simplifier.get_local_simpset and Classical.get_local_claset, 

681 
respectively, in order to see the context dependent fields! 

682 

16251
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

683 
* File.sysify_path and File.quote_sysify path have been replaced by 
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

684 
File.platform_path and File.shell_path (with appropriate hooks). This 
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

685 
provides a clean interface for unusual systems where the internal and 
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

686 
external process view of file names are different. 
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

687 

17166  688 
* ML functions legacy_bindings and use_legacy_bindings produce ML fact 
689 
bindings for all theorems stored within a given theory; this may help 

690 
in porting nonIsar theories to Isar ones, while keeping ML proof 

691 
scripts for the time being. 

692 

16234  693 

694 
*** System *** 

695 

696 
* Allow symlinks to all proper Isabelle executables (Isabelle, 

697 
isabelle, isatool etc.). 

698 

699 
* ISABELLE_DOC_FORMAT setting specifies preferred document format (for 

700 
isatool doc, isatool mkdir, display_drafts etc.). 

701 

702 
* isatool usedir: option f allows specification of the ML file to be 

703 
used by Isabelle; default is ROOT.ML. 

704 

16251
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

705 
* New isatool version outputs the version identifier of the Isabelle 
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

706 
distribution being used. 
121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

707 

121dc80d120a
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
wenzelm
parents:
16234
diff
changeset

708 
* HOL: new isatool dimacs2hol converts files in DIMACS CNF format 
16234  709 
(containing Boolean satisfiability problems) into Isabelle/HOL 
710 
theories. 

15703  711 

712 

14655
8a95abf87dd3
Pure: considerably improved version of 'constdefs' command;
wenzelm
parents:
14624
diff
changeset

713 

14606  714 
New in Isabelle2004 (April 2004) 
715 
 

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

716 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14136
diff
changeset

717 
*** General *** 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14136
diff
changeset

718 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

719 
* Provers/order.ML: new efficient reasoner for partial and linear orders. 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

720 
Replaces linorder.ML. 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

721 

14606  722 
* Pure: Greek letters (except small lambda, \<lambda>), as well as Gothic 
723 
(\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and Euler 

14173  724 
(\<a>...\<z>), are now considered normal letters, and can therefore 
725 
be used anywhere where an ASCII letter (a...zA...Z) has until 

726 
now. COMPATIBILITY: This obviously changes the parsing of some 

727 
terms, especially where a symbol has been used as a binder, say 

728 
'\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed 

729 
as an identifier. Fix it by inserting a space around former 

730 
symbols. Call 'isatool fixgreek' to try to fix parsing errors in 

731 
existing theory and ML files. 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
14136
diff
changeset

732 

14237  733 
* Pure: Macintosh and Windows linebreaks are now allowed in theory files. 
734 

14731  735 
* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
736 
allowed in identifiers. Similar to Greek letters \<^isub> is now considered 

737 
a normal (but invisible) letter. For multiple letter subscripts repeat 

738 
\<^isub> like this: x\<^isub>1\<^isub>2. 

14233  739 

14333  740 
* Pure: There are now sub/superscripts that can span more than one 
741 
character. Text between \<^bsub> and \<^esub> is set in subscript in 

14606  742 
ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in 
743 
superscript. The new control characters are not identifier parts. 

14333  744 

14561
c53396af770e
* raw control symbols are of the form \<^raw:...> now.
schirmer
parents:
14556
diff
changeset

745 
* Pure: Controlsymbols of the form \<^raw:...> will literally print the 
14606  746 
content of "..." to the latex file instead of \isacntrl... . The "..." 
747 
may consist of any printable characters excluding the end bracket >. 

14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14333
diff
changeset

748 

14237  749 
* Pure: Using new Isar command "finalconsts" (or the ML functions 
750 
Theory.add_finals or Theory.add_finals_i) it is now possible to 

751 
declare constants "final", which prevents their being given a definition 

752 
later. It is useful for constants whose behaviour is fixed axiomatically 

14224  753 
rather than definitionally, such as the metalogic connectives. 
754 

14606  755 
* Pure: 'instance' now handles general arities with general sorts 
756 
(i.e. intersections of classes), 

14503
255ad604e08e
Added check that Theory.ML does not occur in the files section of the theory
skalberg
parents:
14480
diff
changeset

757 

14547  758 
* Presentation: generated HTML now uses a CSS style sheet to make layout 
14731  759 
(somewhat) independent of content. It is copied from lib/html/isabelle.css. 
14547  760 
It can be changed to alter the colors/layout of generated pages. 
761 

14556
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset

762 

14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

763 
*** Isar *** 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

764 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset

765 
* Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac, 
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset

766 
cut_tac, subgoal_tac and thin_tac: 
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

767 
 Now understand static (Isar) contexts. As a consequence, users of Isar 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

768 
locales are no longer forced to write Isar proof scripts. 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

769 
For details see Isar Reference Manual, paragraph 4.3.2: Further tactic 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

770 
emulations. 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

771 
 INCOMPATIBILITY: names of variables to be instantiated may no 
14211
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

772 
longer be enclosed in quotes. Instead, precede variable name with `?'. 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

773 
This is consistent with the instantiation attribute "where". 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

774 

14257
a7ef3f7588c5
Type inference bug in Isar attributes "where" and "of" fixed.
ballarin
parents:
14255
diff
changeset

775 
* Attributes "where" and "of": 
14285
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset

776 
 Now take type variables of instantiated theorem into account when reading 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset

777 
the instantiation string. This fixes a bug that caused instantiated 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset

778 
theorems to have too special types in some circumstances. 
92ed032e83a1
Isar: where attribute supports instantiation of type vars.
ballarin
parents:
14283
diff
changeset

779 
 "where" permits explicit instantiations of type variables. 
14257
a7ef3f7588c5
Type inference bug in Isar attributes "where" and "of" fixed.
ballarin
parents:
14255
diff
changeset

780 

14556
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset

781 
* Calculation commands "moreover" and "also" no longer interfere with 
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset

782 
current facts ("this"), admitting arbitrary combinations with "then" 
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset

783 
and derived forms. 
14283  784 

14211
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

785 
* Locales: 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

786 
 Goal statements involving the context element "includes" no longer 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

787 
generate theorems with internal delta predicates (those ending on 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

788 
"_axioms") in the premise. 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

789 
Resolve particular premise with <locale>.intro to obtain old form. 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

790 
 Fixed bug in type inference ("unify_frozen") that prevented mix of target 
7286c187596d
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14199
diff
changeset

791 
specification and "includes" elements in goal statement. 
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14243
diff
changeset

792 
 Rule sets <locale>.intro and <locale>.axioms no longer declared as 
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14243
diff
changeset

793 
[intro?] and [elim?] (respectively) by default. 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset

794 
 Experimental command for instantiation of locales in proof contexts: 
14551  795 
instantiate <label>[<attrs>]: <loc> 
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset

796 
Instantiates locale <loc> and adds all its theorems to the current context 
14551  797 
taking into account their attributes. Label and attrs are optional 
798 
modifiers, like in theorem declarations. If present, names of 

799 
instantiated theorems are qualified with <label>, and the attributes 

800 
<attrs> are applied after any attributes these theorems might have already. 

801 
If the locale has assumptions, a chained fact of the form 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14503
diff
changeset

802 
"<loc> t1 ... tn" is expected from which instantiations of the parameters 
14551  803 
are derived. The command does not support oldstyle locales declared 
804 
with "locale (open)". 

805 
A few (very simple) examples can be found in FOL/ex/LocaleInst.thy. 

14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

806 

dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

807 
* HOL: Tactic emulation methods induct_tac and case_tac understand static 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

808 
(Isar) contexts. 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
14173
diff
changeset

809 

14556
c5078f6c99a9
* Calculation commands "moreover" and "also" no longer interfere with
wenzelm
parents:
14551
diff
changeset

810 

14136  811 
*** HOL *** 
812 

14624  813 
* Proof import: new image HOL4 contains the imported library from 
814 
the HOL4 system with about 2500 theorems. It is imported by 

815 
replaying proof terms produced by HOL4 in Isabelle. The HOL4 image 

816 
can be used like any other Isabelle image. See 

817 
HOL/Import/HOL/README for more information. 

818 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

819 
* Simplifier: 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

820 
 Much improved handling of linear and partial orders. 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

821 
Reasoners for linear and partial orders are set up for type classes 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

822 
"linorder" and "order" respectively, and are added to the default simpset 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

823 
as solvers. This means that the simplifier can build transitivity chains 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

824 
to solve goals from the assumptions. 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

825 
 INCOMPATIBILITY: old proofs break occasionally. Typically, applications 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

826 
of blast or auto after simplification become unnecessary because the goal 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

827 
is solved by simplification already. 
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
14389
diff
changeset

828 

14731  829 
* Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, 
14389  830 
all proved in axiomatic type classes for semirings, rings and fields. 
831 

832 
* Numerics: 

833 
 Numeric types (nat, int, and in HOLComplex rat, real, complex, etc.) are 

14731  834 
now formalized using the Ring_and_Field theory mentioned above. 
14389  835 
 INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently 
836 
than before, because now they are set up once in a generic manner. 

14731  837 
 INCOMPATIBILITY: many typespecific arithmetic laws have gone. 
14480  838 
Look for the general versions in Ring_and_Field (and Power if they concern 
839 
exponentiation). 

14389  840 

14401  841 
* Type "rat" of the rational numbers is now available in HOLComplex. 
14389  842 

14255  843 
* Records: 
844 
 Record types are now by default printed with their type abbreviation 

845 
instead of the list of all field types. This can be configured via 

846 
the reference "print_record_type_abbr". 

14731  847 
 Simproc "record_upd_simproc" for simplification of multiple updates added 
14255  848 
(not enabled by default). 
14427  849 
 Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. 
850 
EX x. x = sel r to True (not enabled by default). 

14255  851 
 Tactic "record_split_simp_tac" to split and simplify records added. 
14731  852 

14136  853 
* 'specification' command added, allowing for definition by 
14224  854 
specification. There is also an 'ax_specification' command that 
855 
introduces the new constants axiomatically. 

14136  856 

14375  857 
* arith(_tac) is now able to generate counterexamples for reals as well. 
858 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14398
diff
changeset

859 
* HOLAlgebra: new locale "ring" for noncommutative rings. 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
14398
diff
changeset

860 

14243  861 
* HOLex: InductiveInvariant_examples illustrates advanced recursive function 
14610  862 
definitions, thanks to Sava Krsti\'{c} and John Matthews. 
863 

14731  864 
* HOLMatrix: a first theory for matrices in HOL with an application of 
14610  865 
matrix theory to linear programming. 
14136  866 

14380  867 
* Unions and Intersections: 
15119  868 
The latex output syntax of UN and INT has been changed 
869 
from "\Union x \in A. B" to "\Union_{x \in A} B" 

870 
i.e. the index formulae has become a subscript. 

871 
Similarly for "\Union x. B", and for \Inter instead of \Union. 

14380  872 

14418  873 
* Unions and Intersections over Intervals: 
14731  874 
There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is 
875 
also an xsymbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" 

14418  876 
like in normal math, and corresponding versions for < and for intersection. 
877 

15677  878 
* HOL/List: Ordering "lexico" is renamed "lenlex" and the standard 
879 
lexicographic dictonary ordering has been added as "lexord". 

880 

14401  881 
* ML: the legacy theory structures Int and List have been removed. They had 
882 
conflicted with ML Basis Library structures having the same names. 

14380  883 

14464  884 
* 'refute' command added to search for (finite) countermodels. Only works 
885 
for a fragment of HOL. The installation of an external SAT solver is 

886 
highly recommended. See "HOL/Refute.thy" for details. 

887 

14602  888 
* 'quickcheck' command: Allows to find counterexamples by evaluating 
889 
formulae under an assignment of free variables to random values. 

890 
In contrast to 'refute', it can deal with inductive datatypes, 

891 
but cannot handle quantifiers. See "HOL/ex/Quickcheck_Examples.thy" 

892 
for examples. 

14464  893 

14606  894 

14536  895 
*** HOLCF *** 
896 

897 
* Streams now come with concatenation and are part of the HOLCF image 

898 

14572  899 

900 

14136  901 
New in Isabelle2003 (May 2003) 
14606  902 
 
14136  903 

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

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

905 

13618  906 
* Provers/simplifier: 
907 

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

911 
the order of assumptions. 

912 

913 
Potential INCOMPATIBILITY: 

914 

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

13618  917 

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

919 

13781  920 
now gives rise to the infinite reduction sequence 
921 

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

923 

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

925 
kind of problem. 

926 

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

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

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

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

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

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

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

13618  934 

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

936 

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

939 
conditions before applying the rewrite rule): 

940 
ML "simp_depth_limit := n" 

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

942 
the simplifier would diverge. 

943 

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

944 
 Accepts free variables as head terms in congruence rules. Useful in Isar. 
13829  945 

13938  946 
 No longer aborts on failed congruence proof. Instead, the 
947 
congruence is ignored. 

948 

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

951 
as HOL/Extraction for some case studies. 

952 

13868  953 
* Pure: The main goal of the proof state is no longer shown by default, only 
954 
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

955 
PG menu: Isabelle/Isar > Settings > Show Main Goal 
13815  956 
(ML: Proof.show_main_goal). 
957 

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

959 
rules whose conclusion matches subgoal 1: 

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

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

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

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

964 
(ML: ProofGeneral.print_intros()) 

965 

966 
* Pure: New flag trace_unify_fail causes unification to print 

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

969 
assumption failed. 

970 

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

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

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

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

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

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

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

978 

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

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

980 
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

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

982 

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

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

984 
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

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

988 
be given (the default is 40); 

989 

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

991 
(batchmode only); 

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

992 

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

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

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

995 
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

996 

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

999 
for slight decrease in efficiency; 

1000 

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

1003 

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

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

1005 
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

1006 

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

1007 

13158  1008 
*** HOL *** 
1009 

13899  1010 
* arith(_tac) 
1011 

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

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

1014 
of quantifierfree linear arithmetic. 

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

1016 

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

1018 

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

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

14731  1021 
Presburger arithmetic can also be called explicitly via presburger(_tac). 
13899  1022 

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

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

1025 

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

1027 
are distributed over a sum of terms; 

1028 

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

14731  1031 
"<=", "<" and "="). 
1032 

1033 
* function INCOMPATIBILITIES: Pisets have been redefined and moved from main 

13587  1034 
HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp"; 
1035 

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

1038 

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

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

1040 
Finite_Set); 
13492  1041 

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

1044 

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

1047 

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

1050 
of the empty set. 

1051 

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

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

1055 
Univariate Polynomials). Contributions welcome; 

13960  1056 

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

1058 

14731  1059 
* Complex: new directory of the complex numbers with numeric constants, 
1060 
nonstandard complex numbers, and some complex analysis, standard and 

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

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

1062 

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

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

1064 

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

1066 
Fleuriot); 
13960  1067 

13549  1068 
* Real/HahnBanach: updated and adapted to locales; 
1069 

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

13872  1072 

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

1074 

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

1077 

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

1080 
classes, interfaces, objects,virtual methods, static methods, 

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

1082 
assignment, exceptions. 

13549  1083 

14011  1084 

13549  1085 
*** ZF *** 
1086 

15154  1087 
* ZF/Constructible: consistency proof for AC (Gdel's constructible 
13549  1088 
universe, etc.); 
1089 

13872  1090 
* Main ZF: virtually all theories converted to newstyle format; 
13518  1091 

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

1092 

13478  1093 
*** ML *** 
1094 

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

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

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

1098 

1099 
* Pure: improved error reporting of simprocs; 

1100 

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

1102 
up simprocs; 

1103 

1104 

13953  1105 
*** Document preparation *** 
1106 

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

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

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

1110 

14731  1111 
* minimized dependencies of isabelle.sty and isabellesym.sty on 
13953  1112 
other packages 
1113 

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

1115 
broke \Rightarrow) 

1116 

14731  1117 
* normal size for \<zero>...\<nine> (uses \mathbf instead of 
13954  1118 
textcomp package) 
13953  1119 

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

1120 

14572  1121 

12984  1122 
New in Isabelle2002 (March 2002) 
1123 
 

11474  1124 

11572  1125 
*** Document preparation *** 
1126 

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

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

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

1129 
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

1130 
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

1131 
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

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

1133 

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

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

1135 
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

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

1137 

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

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

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

1140 

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

1143 

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

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

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

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

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

1152 
isatool document copies the Isabelle style files to the target 

1153 
location; 

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

1154 

11572  1155 

11633  1156 
*** Isar *** 
1157 

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

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

1161 
 'induct' method divinates rule instantiation from the inductive 

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

1163 
instantiation of cases; 

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

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

1166 
rules without further ado; 

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

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

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

1170 
statement becomes is included in the hypothesis, avoiding the 

1171 
slightly cumbersome show "PROP ?case" form; 

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

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

1174 
rules stemming from inductive sets to be applied in unstructured 

1175 
scripts, while still benefitting from proper handling of nonatomic 

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

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

1178 
 'induct' proper support for mutual induction involving nonatomic 

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

1180 
below); 

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

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

1183 
 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

1184 
 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

1185 
 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

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

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

1188 
 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

1189 

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

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

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

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

1193 
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

1194 
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

1195 
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

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

1197 

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

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

1199 

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

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

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

1202 

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

1203 
* Pure: proper integration with ``locales''; unlike the original 
15154  1204 
version by Florian Kammller, Isar locales package highlevel proof 
12078
4eb8061286e5
* Isar/Pure: proper integration with ``locales''; unlike the original
wenzelm
parents:
12034
diff
changeset

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

1209 
some examples; 

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

1210 

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

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

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

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

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

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

1216 

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

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

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

1221 
the context elements being discharged in the obvious way; 

1222 

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

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

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

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

1227 
``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

1228 

11722  1229 
* Pure: renamed "antecedent" case to "rule_context"; 
1230 

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

1233 
use hardwired "Trueprop"; 

1234 

11738  1235 
* Pure: added 'corollary' command; 
1236 

11722  1237 
* Pure: fixed 'token_translation' command; 
1238 

11899  1239 
* Pure: removed obsolete 'exported' attribute; 
1240 

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

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

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

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

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

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

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

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

1250 

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

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

1252 
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

1253 
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

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

1255 

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

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

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

1258 

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

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

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

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

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

1263 

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

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

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

1266 

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

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

1268 
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

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

1270 

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

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

1272 
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

1273 
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

1274 

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

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

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

1277 
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

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

1279 
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

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

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

1282 

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

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

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

1285 

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

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

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

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

1289 

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

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

1291 

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

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

1297 

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

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

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

1300 

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

1301 

11474  1302 
*** HOL *** 
1303 

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

1306 

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

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

1309 

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

1311 
binary representation internally; 

1312 

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

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

1315 

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

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

1317 
are some hints on converting existing sources: 
11702  1318 

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

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

1321 
to be spaced properly; 

1322 

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

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

1325 

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

1327 

1328 
 remove all special provisions on numerals in proofs; 

1329 

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

12736  1333 
* HOL: symbolic syntax for x^2 (numeral 2); 
1334 

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

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

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

1337 
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

1338 
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

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

1340 

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

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

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

1345 
declared as simp by default; 

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

1346 
 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

1347 
qualified)  potential INCOMPATIBILITY; 
12280  1348 
 removed "make_scheme" operations (use "make" with "extend")  
1349 
INCOMPATIBILITY; 

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

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

1356 

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

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

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

1359 
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

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

1361 

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

13824  1364 
* HOL: consolidated and renamed several theories. In particular: 
14731  1365 
Ord.thy has been absorbed into HOL.thy 
1366 
String.thy has been absorbed into List.thy 

1367 

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

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

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

1370 

11657  1371 
* HOL: linorder_less_split superseded by linorder_cases; 
1372 

12917  1373 
* HOL/List: "nodups" renamed to "distinct"; 
12889  1374 

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

11437  1378 

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

1381 

1382 
delSWrapper "split_all_tac" 

1383 
addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac) 

1384 

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

11474  1386 
MAY FAIL; 
11361  1387 

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

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

1391 
necessary to attach explicit type constraints; 

11307  1392 

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

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

12489  1396 

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

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

1398 
expressions; 
11474  1399 

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

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

1401 
of "lam"  INCOMPATIBILITY; 
11474  1402 

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

1405 
renamed "Product_Type.unit"; 

11611  1406 

12564  1407 
* HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl 
1408 

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

02eb40cde931
* HOL: removed ob 