author  huffman 
Tue, 12 Jul 2005 18:20:44 +0200  
changeset 16776  a3899ac14a1c 
parent 16718  70c94b82c556 
child 16799  978dcf30c3dd 
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 

22 
nonIsar theories. 

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 

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

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 

54 
* There is now a flag to control hiding of proofs and some other 

55 
commands (such as 'ML' or 'parse/print_translation') in document 

56 
output. Hiding is enabled by default, and can be disabled by the 

57 
option 'H false' of isatool usedir or by resetting the reference 

58 
variable IsarOutput.hide_commands in ML. Additional commands to be 

59 
hidden may be declared using IsarOutput.add_hidden_commands. 

60 

15979  61 
* Several new antiquotation: 
62 

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

64 

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

66 

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

15979  69 

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

16234  71 
theorem applying a "style" to it 
72 

73 
Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of 

74 
definitions, equations, inequations etc., 'concl' printing only the 

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

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

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

78 
document practical applications. 

79 

80 

81 
*** Pure *** 

82 

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

84 
automatic typeinference of declared constants; additional support for 

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

86 
isarref manual. Potential INCOMPATIBILITY: need to observe strictly 

87 
sequential dependencies of definitions within a single 'constdefs' 

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

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

90 

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

92 
indexed syntax provides a notational device for subscripted 

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

94 
expressions. Secondly, in a local context with structure 

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

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

97 
show_structs controls printing of implicit structures. Typical 

98 
applications of these concepts involve record types and locales. 

99 

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

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

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

103 

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

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

106 
parsing/printing, see also isarref manual. 

107 

108 
* Improved internal renaming of symbolic identifiers  attach primes 

109 
instead of base 26 numbers. 

110 

111 
* New flag show_question_marks controls printing of leading question 

112 
marks in schematic variable names. 

113 

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

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

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

117 

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

119 
by simp 

120 

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

122 

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

124 
annotations as "(00...)". 

125 

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

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

128 
Before that distinction was only partially implemented via type class 

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

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

131 
exotic syntax specifications may require further adaption 

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

133 

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

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

136 
rather than 'types'. INCOMPATIBILITY for new objectlogic 

137 
specifications. 

138 

139 
* Simplifier: can now control the depth to which conditional rewriting 

140 
is traced via the PG menu Isabelle > Settings > Trace Simp Depth 

141 
Limit. 

142 

143 
* Simplifier: simplification procedures may now take the current 

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

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

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

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

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

149 
allow for use in a context of fixed variables. 

150 

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

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

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

154 

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

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

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

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

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

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

161 

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

163 
selections of theorems in named facts via index ranges. 

164 

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

165 
* More efficient treatment of intermediate checkpoints in interactive 
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset

166 
theory development. 
b2687ce38433
* Pure: get_thm interface expects datatype thmref;
wenzelm
parents:
16456
diff
changeset

167 

16234  168 

169 
*** Locales *** 

170 

171 
* New commands for the interpretation of locale expressions in 

172 
theories ('interpretation') and proof contexts ('interpret'). These 

173 
take an instantiation of the locale parameters and compute proof 

174 
obligations from the instantiated specification. After the 

175 
obligations have been discharged, the instantiated theorems of the 

176 
locale are added to the theory or proof context. Interpretation is 

177 
smart in that already active interpretations do not occur in proof 

178 
obligations, neither are instantiated theorems stored in duplicate. 

179 
Use print_interps to inspect active interpretations of a particular 

180 
locale. For details, see the Isar Reference manual. 

181 

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

183 
'interpret' instead. 

184 

185 
* Proper static binding of attribute syntax  i.e. types / terms / 

186 
facts mentioned as arguments are always those of the locale definition 

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

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

189 
to attribute arguments as expected. 

190 

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

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

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

194 
Attribute implementations need to cooperate properly with the static 

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

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

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

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

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

200 
values to argument tokens explicitly. 

201 

202 
* New context element "constrains" adds type constraints to parameters  

203 
there is no logical significance. 

204 

205 
* Context expressions: renaming parameters permits syntax 

206 
redeclaration as well. 

207 

208 
* Locale definition: 'includes' now disallowed. 

209 

210 
* Changed parameter management in theorem generation for long goal 

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

212 
theorem statement in rare situations. 

213 

214 
* Attributes 'induct' and 'cases': type or set names may now be 

215 
locally fixed variables as well. 

15703  216 

217 
* Antiquotations now provide the option 'locale=NAME' to specify an 

16234  218 
alternative context used for evaluating and printing the subsequent 
219 
argument, as in @{thm [locale=LC] fold_commute}, for example. 

220 

221 

222 
*** Provers *** 

223 

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

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

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

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

228 
still available as 'simplesubst'. 

229 

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

231 
and quasi orders. 

232 

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

234 
reflexivetransitive closure of relations. 

235 

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

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

238 

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

240 
is peformed already. Objectlogics merely need to finish their 

241 
initial simpset configuration as before. INCOMPATIBILITY. 

15703  242 

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

243 

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

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

245 

16234  246 
* Symbolic syntax of Hilbert Choice Operator is now as follows: 
14878  247 

248 
syntax (epsilon) 

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

250 

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

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

254 
becomes available as variable, constant etc. INCOMPATIBILITY, 

255 

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

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

258 
is \<ge>. 

259 

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

261 
instead of ":". 

262 

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

264 

265 
Old New 

266 
{..n(} {..<n} 

267 
{)n..} {n<..} 

268 
{m..n(} {m..<n} 

269 
{)m..n} {m<..n} 

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

271 

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

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

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

15046  275 

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

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

278 

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

281 
now either "SUM x:A. e" or "\<Sum>x \<in> A. e". 

282 

283 
Some new syntax forms are available: 

284 

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

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

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

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

289 

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

291 
function "Summation", which has been discontinued. 

292 

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

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

295 
(insert F x)'. 

296 

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

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

299 
typedefs, inductive datatypes and recursion. 

300 

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

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

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

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

305 
in unstructured proof scripts. 

306 

307 
* Reworked implementation of records. Improved scalability for 

308 
records with many fields, avoiding performance problems for type 

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

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

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

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

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

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

315 
<record_name>_ext_type. 

316 

317 
Flag record_quick_and_dirty_sensitive can be enabled to skip the 

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

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

320 
quite long. 

321 

322 
New simproc record_upd_simproc for simplification of multiple record 

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

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

325 
occasionally, since simplification is more powerful by default. 

326 

327 
* Simplifier: automatically reasons about transitivity chains 

328 
involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics 

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

330 
old proofs break occasionally as simplification may now solve more 

331 
goals than previously. 

332 

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

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

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

336 
just like y <= x. 

337 

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

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

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

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

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

343 
enabled/disabled by the reference use_let_simproc. Potential 

344 
INCOMPATIBILITY since simplification is more powerful by default. 

15776  345 

16563  346 
* Classical reasoning: the meson method now accepts theorems as arguments. 
347 

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

348 

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

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

350 

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

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

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

354 

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

355 

14885  356 
*** ZF *** 
357 

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

360 
of a homomorphism). 

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

361 

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

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

15703  365 

366 

367 
*** ML *** 

368 

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

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

373 
accordingly, while Option.map replaces apsome. 

15973  374 

16151  375 
* The exception LIST has been given up in favour of the standard 
16234  376 
exceptions Empty and Subscript, as well as Library.UnequalLengths. 
377 
Function like Library.hd and Library.tl are superceded by the standard 

378 
hd and tl functions etc. 

379 

380 
A number of basic functions are now no longer exported to the ML 

381 
toplevel, as they are variants of standard functions. The following 

382 
suggests how one can translate existing code: 

15973  383 

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

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

386 
last_elem xs = List.last xs 

387 
flat xss = List.concat xss 

16234  388 
seq fs = List.app fs 
15973  389 
partition P xs = List.partition P xs 
390 
filter P xs = List.filter P xs 

391 
mapfilter f xs = List.mapPartial f xs 

392 

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

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

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

398 
result of Pretty.string_of/str_of and derived functions 

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

400 
easy composition of diagnostic messages etc. Programmers rarely need 

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

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

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

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

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

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

407 
have no effect. 

408 

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

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

412 

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

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

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

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

417 
(both increase the runtime). 

15703  418 

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

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

421 

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

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

423 
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

424 
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

425 
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

426 
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

427 
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

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

429 

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

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

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

435 
name; NameSpace.extend is superceded by context dependent 

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

437 
the naming context. Especially note Theory.restore_naming and 

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

439 
Theory.add_path is no longer sufficient to recover from 

440 
Theory.absolute_path in particular. 

441 

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

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

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

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

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

447 
with earlier declarations. 

16151  448 

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

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

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

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

452 

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

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

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

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

456 
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

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

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

459 

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

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

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

462 

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

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

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

465 

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

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

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

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

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

470 

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

471 
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

472 
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

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

474 

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

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

476 
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

477 
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

478 
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

479 

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

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

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

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

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

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

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

486 
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

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

488 

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

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

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

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

492 

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

16151  496 

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

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

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

499 

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

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

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

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

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

504 

16718  505 
* Pure: print_tac now outputs the goal through the trace channel. 
506 

15703  507 
* Provers: Simplifier and Classical Reasoner now support proof context 
16234  508 
dependent plugins (simprocs, solvers, wrappers etc.). These extra 
509 
components are stored in the theory and patched into the 

510 
simpset/claset when used in an Isar proof context. Context dependent 

511 
components are maintained by the following theory operations: 

512 

513 
Simplifier.add_context_simprocs 

514 
Simplifier.del_context_simprocs 

515 
Simplifier.set_context_subgoaler 

516 
Simplifier.reset_context_subgoaler 

517 
Simplifier.add_context_looper 

518 
Simplifier.del_context_looper 

519 
Simplifier.add_context_unsafe_solver 

520 
Simplifier.add_context_safe_solver 

521 

522 
Classical.add_context_safe_wrapper 

523 
Classical.del_context_safe_wrapper 

524 
Classical.add_context_unsafe_wrapper 

525 
Classical.del_context_unsafe_wrapper 

526 

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

528 
local_simpset_of and local_claset_of to instead of the primitive 

529 
Simplifier.get_local_simpset and Classical.get_local_claset, 

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

531 

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

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

533 
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

534 
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

535 
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

536 

16234  537 

538 
*** System *** 

539 

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

541 
isabelle, isatool etc.). 

542 

543 
* ISABELLE_DOC_FORMAT setting specifies preferred document format (for 

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

545 

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

547 
used by Isabelle; default is ROOT.ML. 

548 

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

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

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

551 

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

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

15703  555 

556 

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

557 

14606  558 
New in Isabelle2004 (April 2004) 
559 
 

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

560 

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

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

562 

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

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

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

565 

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

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

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

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

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

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

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

575 
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

576 

14237  577 
* Pure: Macintosh and Windows linebreaks are now allowed in theory files. 
578 

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

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

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

14233  583 

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

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

14333  588 

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

589 
* Pure: Controlsymbols of the form \<^raw:...> will literally print the 
14606  590 
content of "..." to the latex file instead of \isacntrl... . The "..." 
591 
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

592 

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

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

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

14224  597 
rather than definitionally, such as the metalogic connectives. 
598 

14606  599 
* Pure: 'instance' now handles general arities with general sorts 
600 
(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

601 

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

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

606 

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

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

608 

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

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

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

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

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

613 
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

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

615 
 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

616 
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

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

618 

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

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

620 
 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

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

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

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

624 

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

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

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

627 
and derived forms. 
14283  628 

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

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

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

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

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

633 
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

634 
 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

635 
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

636 
 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

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

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

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

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

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

645 
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

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

649 
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

650 

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

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

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

653 

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

654 

14136  655 
*** HOL *** 
656 

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

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

660 
can be used like any other Isabelle image. See 

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

662 

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

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

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

665 
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

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

667 
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

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

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

670 
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

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

672 

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

676 
* Numerics: 

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

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

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

14389  684 

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

14255  687 
* Records: 
688 
 Record types are now by default printed with their type abbreviation 

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

690 
the reference "print_record_type_abbr". 

14731  691 
 Simproc "record_upd_simproc" for simplification of multiple updates added 
14255  692 
(not enabled by default). 
14427  693 
 Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. 
694 
EX x. x = sel r to True (not enabled by default). 

14255  695 
 Tactic "record_split_simp_tac" to split and simplify records added. 
14731  696 

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

14136  700 

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

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

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

704 

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

14731  708 
* HOLMatrix: a first theory for matrices in HOL with an application of 
14610  709 
matrix theory to linear programming. 
14136  710 

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

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

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

14380  716 

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

14418  720 
like in normal math, and corresponding versions for < and for intersection. 
721 

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

724 

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

14380  727 

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

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

731 

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

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

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

736 
for examples. 

14464  737 

14606  738 

14536  739 
*** HOLCF *** 
740 

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

742 

14572  743 

744 

14136  745 
New in Isabelle2003 (May 2003) 
14606  746 
 
14136  747 

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

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

749 

13618  750 
* Provers/simplifier: 
751 

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

755 
the order of assumptions. 

756 

757 
Potential INCOMPATIBILITY: 

758 

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

13618  761 

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

763 

13781  764 
now gives rise to the infinite reduction sequence 
765 

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

767 

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

769 
kind of problem. 

770 

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

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

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

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

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

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

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

13618  778 

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

780 

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

783 
conditions before applying the rewrite rule): 

784 
ML "simp_depth_limit := n" 

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

786 
the simplifier would diverge. 

787 

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

788 
 Accepts free variables as head terms in congruence rules. Useful in Isar. 
13829  789 

13938  790 
 No longer aborts on failed congruence proof. Instead, the 
791 
congruence is ignored. 

792 

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

795 
as HOL/Extraction for some case studies. 

796 

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

799 
PG menu: Isabelle/Isar > Settings > Show Main Goal 
13815  800 
(ML: Proof.show_main_goal). 
801 

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

803 
rules whose conclusion matches subgoal 1: 

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

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

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

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

808 
(ML: ProofGeneral.print_intros()) 

809 

810 
* Pure: New flag trace_unify_fail causes unification to print 

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

813 
assumption failed. 

814 

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

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

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

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

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

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

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

822 

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

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

824 
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

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

826 

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

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

828 
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

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

832 
be given (the default is 40); 

833 

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

835 
(batchmode only); 

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

836 

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

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

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

839 
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

840 

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

843 
for slight decrease in efficiency; 

844 

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

847 

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

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

849 
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

850 

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

851 

13158  852 
*** HOL *** 
853 

13899  854 
* arith(_tac) 
855 

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

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

858 
of quantifierfree linear arithmetic. 

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

860 

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

862 

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

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

14731  865 
Presburger arithmetic can also be called explicitly via presburger(_tac). 
13899  866 

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

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

869 

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

871 
are distributed over a sum of terms; 

872 

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

14731  875 
"<=", "<" and "="). 
876 

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

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

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

882 

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

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

884 
Finite_Set); 
13492  885 

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

888 

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

891 

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

894 
of the empty set. 

895 

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

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

899 
Univariate Polynomials). Contributions welcome; 

13960  900 

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

902 

14731  903 
* Complex: new directory of the complex numbers with numeric constants, 
904 
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

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

906 

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

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

908 

14731  909 
* 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

910 
Fleuriot); 
13960  911 

13549  912 
* Real/HahnBanach: updated and adapted to locales; 
913 

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

13872  916 

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

918 

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

921 

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

924 
classes, interfaces, objects,virtual methods, static methods, 

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

926 
assignment, exceptions. 

13549  927 

14011  928 

13549  929 
*** ZF *** 
930 

15154  931 
* ZF/Constructible: consistency proof for AC (Gdel's constructible 
13549  932 
universe, etc.); 
933 

13872  934 
* Main ZF: virtually all theories converted to newstyle format; 
13518  935 

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

936 

13478  937 
*** ML *** 
938 

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

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

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

942 

943 
* Pure: improved error reporting of simprocs; 

944 

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

946 
up simprocs; 

947 

948 

13953  949 
*** Document preparation *** 
950 

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

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

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

954 

14731  955 
* minimized dependencies of isabelle.sty and isabellesym.sty on 
13953  956 
other packages 
957 

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

959 
broke \Rightarrow) 

960 

14731  961 
* normal size for \<zero>...\<nine> (uses \mathbf instead of 
13954  962 
textcomp package) 
13953  963 

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

964 

14572  965 

12984  966 
New in Isabelle2002 (March 2002) 
967 
 

11474  968 

11572  969 
*** Document preparation *** 
970 

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

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

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

973 
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

974 
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

975 
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

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

977 

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

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

979 
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

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

981 

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

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

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

984 

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

987 

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

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

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

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

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

996 
isatool document copies the Isabelle style files to the target 

997 
location; 

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

998 

11572  999 

11633  1000 
*** Isar *** 
1001 

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

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

1005 
 'induct' method divinates rule instantiation from the inductive 

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

1007 
instantiation of cases; 

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

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

1010 
rules without further ado; 

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

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

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

1014 
statement becomes is included in the hypothesis, avoiding the 

1015 
slightly cumbersome show "PROP ?case" form; 

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

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

1018 
rules stemming from inductive sets to be applied in unstructured 

1019 
scripts, while still benefitting from proper handling of nonatomic 

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

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

1022 
 'induct' proper support for mutual induction involving nonatomic 

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

1024 
below); 

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

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

1027 
 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

1028 
 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

1029 
 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

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

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

1032 
 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

1033 

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

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

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

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

1037 
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

1038 
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

1039 
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

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

1041 

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

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

1043 

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

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

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

1046 

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

1047 
* Pure: proper integration with ``locales''; unlike the original 
15154  1048 
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

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

1053 
some examples; 

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

1054 

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

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

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

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

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

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

1060 

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

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

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

1065 
the context elements being discharged in the obvious way; 

1066 

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

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

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

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

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

1072 

11722  1073 
* Pure: renamed "antecedent" case to "rule_context"; 
1074 

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

1077 
use hardwired "Trueprop"; 

1078 

11738  1079 
* Pure: added 'corollary' command; 
1080 

11722  1081 
* Pure: fixed 'token_translation' command; 
1082 

11899  1083 
* Pure: removed obsolete 'exported' attribute; 
1084 

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

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

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

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

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

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

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

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

1094 

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

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

1096 
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

1097 
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

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

1099 

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

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

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

1102 

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

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

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

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

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

1107 

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

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

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

1110 

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

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

1112 
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

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

1114 

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

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

1116 
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

1117 
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

1118 

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

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

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

1121 
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

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

1123 
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

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

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

1126 

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

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

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

1129 

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

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

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

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

1133 

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

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

1135 

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

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

1141 

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

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

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

1144 

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

1145 

11474  1146 
*** HOL *** 
1147 

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

1150 

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

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

1153 

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

1155 
binary representation internally; 

1156 

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

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

1159 

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

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

1161 
are some hints on converting existing sources: 
11702  1162 

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

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

1165 
to be spaced properly; 

1166 

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

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

1169 

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

1171 

1172 
 remove all special provisions on numerals in proofs; 

1173 

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

12736  1177 
* HOL: symbolic syntax for x^2 (numeral 2); 
1178 

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

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

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

1181 
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

1182 
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

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

1184 

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

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

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

1189 
declared as simp by default; 

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

1190 
 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

1191 
qualified)  potential INCOMPATIBILITY; 
12280  1192 
 removed "make_scheme" operations (use "make" with "extend")  
1193 
INCOMPATIBILITY; 

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

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

1200 

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

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

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

1203 
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

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

1205 

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

13824  1208 
* HOL: consolidated and renamed several theories. In particular: 
14731  1209 
Ord.thy has been absorbed into HOL.thy 
1210 
String.thy has been absorbed into List.thy 

1211 

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

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

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

1214 

11657  1215 
* HOL: linorder_less_split superseded by linorder_cases; 
1216 

12917  1217 
* HOL/List: "nodups" renamed to "distinct"; 
12889  1218 

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

11437  1222 

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

1225 

1226 
delSWrapper "split_all_tac" 

1227 
addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac) 

1228 

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

11474  1230 
MAY FAIL; 
11361  1231 

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

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

1235 
necessary to attach explicit type constraints; 

11307  1236 

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

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

12489  1240 

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

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

1242 
expressions; 
11474  1243 

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

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

1245 
of "lam"  INCOMPATIBILITY; 
11474  1246 

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

1249 
renamed "Product_Type.unit"; 

11611  1250 

12564  1251 
* HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl 
1252 

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

1255 

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

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

1258 

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

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

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

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

1262 

12734  1263 
* HOLReal: added Complex_Numbers (by Gertrud Bauer); 
1264 

12690  1265 
* HOLHyperreal is now a logic image; 
1266 

11611  1267 

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

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

1269 

12622  1270 
* Isar: consts/constdefs supports mixfix syntax for continuous 
1271 
operations; 

1272 

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

1274 
HOLCF/ex/Dnat.thy; 

1275 

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

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

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

1279 

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

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

1281 

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

1282 

11474  1283 
*** ZF *** 
1284 

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

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

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

1289 

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

1291 
your theory on Main_ZFC; 

1292 

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

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

12563  1295 

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

1298 

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

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

1301 

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

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

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

1305 

13025  1306 
* ZF: many new theorems about lists, ordinals, etc.; 
12850  1307 

11474  1308 

1309 
*** General *** 

1310 

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

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

1314 
also ref manual for further ML interfaces; 

1315 

1316 
* Pure/axclass: removed obsolete ML interface 

1317 
goal_subclass/goal_arity; 

1318 

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

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

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

1322 
properly; 

1323 

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

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

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

1326 

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

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

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

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

1330 
type variable); 
12280  1331 

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

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

1334 
"type_brackets"; 

1335 

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

11817  1337 
tokens into AST constants; 
11474  1338 

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

1341 
multiple declarations for same syntax element constant; 

1342 

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

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

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

1345 

12280  1346 
* Provers/classical: renamed addaltern to addafter, addSaltern to 
1347 
addSafter; 

1348 

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

1350 
as well; 

12253  1351 

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

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

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

1356 
support requires further installations, e.g. from 

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

1358 

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

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

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

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

1363 

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

1366 

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

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

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

1370 

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

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

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

11551  1376 

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

1379 
isolatin characters may now be used; the related isatools 

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

1381 

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

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

1384 
terminal); 

1385 

11314  1386 

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

1387 

11062  1388 
New in Isabelle992 (February 2001) 
1389 
 

1390 

10224  1391 
*** Overview of INCOMPATIBILITIES *** 
1392 

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

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

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

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

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

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

1401 

10998  1402 
* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, 
1403 
gfp_Tarski to gfp_unfold; 

10224  1404 

10288  1405 
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; 
1406 

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

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

10793  1410 

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

1413 

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

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