author  wenzelm 
Sat, 04 Jun 2005 18:20:00 +0200  
changeset 16234  421c3522f160 
parent 16181  22324687e2d2 
child 16251  121dc80d120a 
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 

20 
will disappear in the next release. Note that there is no change in 

21 
ancient nonIsar theories. 

15130  22 

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

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

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

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

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

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

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

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

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

33 
interpreted as pattern and selects all theorems matching the 

34 
pattern. Available in ProofGeneral under 'ProofGeneral > Find 

35 
Theorems' or Cc Cf. Example: 

36 

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

38 

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

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

41 
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

42 

15703  43 

44 
*** Document preparation *** 

45 

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

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

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

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

51 
DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively). 

52 

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

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

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

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

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

58 
hidden may be declared using IsarOutput.add_hidden_commands. 

59 

15979  60 
* Several new antiquotation: 
61 

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

63 

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

65 

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

15979  68 

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

16234  70 
theorem applying a "style" to it 
71 

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

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

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

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

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

77 
document practical applications. 

78 

79 

80 
*** Pure *** 

81 

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

83 
automatic typeinference of declared constants; additional support for 

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

85 
isarref manual. Potential INCOMPATIBILITY: need to observe strictly 

86 
sequential dependencies of definitions within a single 'constdefs' 

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

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

89 

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

91 
indexed syntax provides a notational device for subscripted 

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

93 
expressions. Secondly, in a local context with structure 

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

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

96 
show_structs controls printing of implicit structures. Typical 

97 
applications of these concepts involve record types and locales. 

98 

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

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

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

102 

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

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

105 
parsing/printing, see also isarref manual. 

106 

107 
* Improved internal renaming of symbolic identifiers  attach primes 

108 
instead of base 26 numbers. 

109 

110 
* New flag show_question_marks controls printing of leading question 

111 
marks in schematic variable names. 

112 

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

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

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

116 

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

118 
by simp 

119 

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

121 

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

123 
annotations as "(00...)". 

124 

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

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

127 
Before that distinction was only partially implemented via type class 

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

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

130 
exotic syntax specifications may require further adaption 

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

132 

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

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

135 
rather than 'types'. INCOMPATIBILITY for new objectlogic 

136 
specifications. 

137 

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

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

140 
Limit. 

141 

142 
* Simplifier: simplification procedures may now take the current 

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

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

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

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

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

148 
allow for use in a context of fixed variables. 

149 

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

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

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

153 

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

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

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

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

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

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

160 

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

162 
selections of theorems in named facts via index ranges. 

163 

164 

165 
*** Locales *** 

166 

167 
* New commands for the interpretation of locale expressions in 

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

169 
take an instantiation of the locale parameters and compute proof 

170 
obligations from the instantiated specification. After the 

171 
obligations have been discharged, the instantiated theorems of the 

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

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

174 
obligations, neither are instantiated theorems stored in duplicate. 

175 
Use print_interps to inspect active interpretations of a particular 

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

177 

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

179 
'interpret' instead. 

180 

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

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

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

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

185 
to attribute arguments as expected. 

186 

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

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

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

190 
Attribute implementations need to cooperate properly with the static 

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

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

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

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

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

196 
values to argument tokens explicitly. 

197 

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

199 
there is no logical significance. 

200 

201 
* Context expressions: renaming parameters permits syntax 

202 
redeclaration as well. 

203 

204 
* Locale definition: 'includes' now disallowed. 

205 

206 
* Changed parameter management in theorem generation for long goal 

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

208 
theorem statement in rare situations. 

209 

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

211 
locally fixed variables as well. 

15703  212 

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

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

216 

217 

218 
*** Provers *** 

219 

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

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

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

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

224 
still available as 'simplesubst'. 

225 

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

227 
and quasi orders. 

228 

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

230 
reflexivetransitive closure of relations. 

231 

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

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

234 

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

236 
is peformed already. Objectlogics merely need to finish their 

237 
initial simpset configuration as before. INCOMPATIBILITY. 

15703  238 

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

239 

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

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

241 

16234  242 
* Symbolic syntax of Hilbert Choice Operator is now as follows: 
14878  243 

244 
syntax (epsilon) 

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

246 

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

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

250 
becomes available as variable, constant etc. INCOMPATIBILITY, 

251 

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

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

254 
is \<ge>. 

255 

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

257 
instead of ":". 

258 

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

260 

261 
Old New 

262 
{..n(} {..<n} 

263 
{)n..} {n<..} 

264 
{m..n(} {m..<n} 

265 
{)m..n} {m<..n} 

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

267 

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

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

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

15046  271 

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

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

274 

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

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

278 

279 
Some new syntax forms are available: 

280 

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

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

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

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

285 

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

287 
function "Summation", which has been discontinued. 

288 

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

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

291 
(insert F x)'. 

292 

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

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

295 
typedefs, inductive datatypes and recursion. 

296 

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

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

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

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

301 
in unstructured proof scripts. 

302 

303 
* Reworked implementation of records. Improved scalability for 

304 
records with many fields, avoiding performance problems for type 

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

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

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

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

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

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

311 
<record_name>_ext_type. 

312 

313 
Flag record_quick_and_dirty_sensitive can be enabled to skip the 

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

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

316 
quite long. 

317 

318 
New simproc record_upd_simproc for simplification of multiple record 

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

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

321 
occasionally, since simplification is more powerful by default. 

322 

323 
* Simplifier: automatically reasons about transitivity chains 

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

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

326 
old proofs break occasionally as simplification may now solve more 

327 
goals than previously. 

328 

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

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

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

332 
just like y <= x. 

333 

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

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

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

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

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

339 
enabled/disabled by the reference use_let_simproc. Potential 

340 
INCOMPATIBILITY since simplification is more powerful by default. 

15776  341 

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

342 

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

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

344 

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

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

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

348 

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

349 

14885  350 
*** ZF *** 
351 

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

354 
of a homomorphism). 

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

355 

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

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

15703  359 

360 

361 
*** ML *** 

362 

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

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

367 
accordingly, while Option.map replaces apsome. 

15973  368 

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

372 
hd and tl functions etc. 

373 

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

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

376 
suggests how one can translate existing code: 

15973  377 

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

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

380 
last_elem xs = List.last xs 

381 
flat xss = List.concat xss 

16234  382 
seq fs = List.app fs 
15973  383 
partition P xs = List.partition P xs 
384 
filter P xs = List.filter P xs 

385 
mapfilter f xs = List.mapPartial f xs 

386 

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

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

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

392 
result of Pretty.string_of/str_of and derived functions 

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

394 
easy composition of diagnostic messages etc. Programmers rarely need 

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

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

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

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

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

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

401 
have no effect. 

402 

403 
* Pure: print_tac now outputs the goal through the trace channel. 

404 

405 
* Isar debugging: new reference Toplevel.debug; default false. Set to 

406 
make printing of exceptions THM, TERM, TYPE and THEORY more verbose. 

15703  407 

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

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

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

413 
name; NameSpace.extend is superceded by context dependent 

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

415 
the naming context. Especially note Theory.restore_naming and 

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

417 
Theory.add_path is no longer sufficient to recover from 

418 
Theory.absolute_path in particular. 

419 

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

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

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

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

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

425 
with earlier declarations. 

16151  426 

427 
* Pure: cases produced by proof methods specify options, where NONE 

16234  428 
means to remove case bindings  INCOMPATIBILITY in 
429 
(RAW_)METHOD_CASES. 

16151  430 

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

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

435 
components are maintained by the following theory operations: 

436 

437 
Simplifier.add_context_simprocs 

438 
Simplifier.del_context_simprocs 

439 
Simplifier.set_context_subgoaler 

440 
Simplifier.reset_context_subgoaler 

441 
Simplifier.add_context_looper 

442 
Simplifier.del_context_looper 

443 
Simplifier.add_context_unsafe_solver 

444 
Simplifier.add_context_safe_solver 

445 

446 
Classical.add_context_safe_wrapper 

447 
Classical.del_context_safe_wrapper 

448 
Classical.add_context_unsafe_wrapper 

449 
Classical.del_context_unsafe_wrapper 

450 

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

452 
local_simpset_of and local_claset_of to instead of the primitive 

453 
Simplifier.get_local_simpset and Classical.get_local_claset, 

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

455 

456 

457 
*** System *** 

458 

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

460 
isabelle, isatool etc.). 

461 

462 
* ISABELLE_DOC_FORMAT setting specifies preferred document format (for 

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

464 

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

466 
used by Isabelle; default is ROOT.ML. 

467 

468 
* HOL: isatool dimacs2hol converts files in DIMACS CNF format 

469 
(containing Boolean satisfiability problems) into Isabelle/HOL 

470 
theories. 

15703  471 

472 

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

473 

14606  474 
New in Isabelle2004 (April 2004) 
475 
 

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

476 

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

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

478 

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

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

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

481 

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

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

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

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

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

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

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

491 
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

492 

14237  493 
* Pure: Macintosh and Windows linebreaks are now allowed in theory files. 
494 

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

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

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

14233  499 

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

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

14333  504 

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

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

508 

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

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

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

14224  513 
rather than definitionally, such as the metalogic connectives. 
514 

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

517 

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

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

522 

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

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

524 

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

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

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

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

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

529 
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

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

531 
 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

532 
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

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

534 

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

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

536 
 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

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

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

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

540 

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

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

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

543 
and derived forms. 
14283  544 

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

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

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

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

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

549 
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

550 
 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

551 
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

552 
 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

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

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

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

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

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

561 
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

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

565 
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

566 

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

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

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

569 

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

570 

14136  571 
*** HOL *** 
572 

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

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

576 
can be used like any other Isabelle image. See 

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

578 

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

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

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

581 
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

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

583 
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

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

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

586 
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

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

588 

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

592 
* Numerics: 

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

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

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

14389  600 

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

14255  603 
* Records: 
604 
 Record types are now by default printed with their type abbreviation 

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

606 
the reference "print_record_type_abbr". 

14731  607 
 Simproc "record_upd_simproc" for simplification of multiple updates added 
14255  608 
(not enabled by default). 
14427  609 
 Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. 
610 
EX x. x = sel r to True (not enabled by default). 

14255  611 
 Tactic "record_split_simp_tac" to split and simplify records added. 
14731  612 

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

14136  616 

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

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

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

620 

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

14731  624 
* HOLMatrix: a first theory for matrices in HOL with an application of 
14610  625 
matrix theory to linear programming. 
14136  626 

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

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

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

14380  632 

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

14418  636 
like in normal math, and corresponding versions for < and for intersection. 
637 

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

640 

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

14380  643 

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

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

647 

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

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

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

652 
for examples. 

14464  653 

14606  654 

14536  655 
*** HOLCF *** 
656 

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

658 

14572  659 

660 

14136  661 
New in Isabelle2003 (May 2003) 
14606  662 
 
14136  663 

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

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

665 

13618  666 
* Provers/simplifier: 
667 

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

671 
the order of assumptions. 

672 

673 
Potential INCOMPATIBILITY: 

674 

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

13618  677 

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

679 

13781  680 
now gives rise to the infinite reduction sequence 
681 

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

683 

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

685 
kind of problem. 

686 

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

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

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

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

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

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

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

13618  694 

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

696 

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

699 
conditions before applying the rewrite rule): 

700 
ML "simp_depth_limit := n" 

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

702 
the simplifier would diverge. 

703 

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

704 
 Accepts free variables as head terms in congruence rules. Useful in Isar. 
13829  705 

13938  706 
 No longer aborts on failed congruence proof. Instead, the 
707 
congruence is ignored. 

708 

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

711 
as HOL/Extraction for some case studies. 

712 

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

715 
PG menu: Isabelle/Isar > Settings > Show Main Goal 
13815  716 
(ML: Proof.show_main_goal). 
717 

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

719 
rules whose conclusion matches subgoal 1: 

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

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

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

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

724 
(ML: ProofGeneral.print_intros()) 

725 

726 
* Pure: New flag trace_unify_fail causes unification to print 

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

729 
assumption failed. 

730 

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

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

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

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

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

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

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

738 

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

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

740 
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

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

742 

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

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

744 
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

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

748 
be given (the default is 40); 

749 

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

751 
(batchmode only); 

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

752 

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

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

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

755 
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

756 

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

759 
for slight decrease in efficiency; 

760 

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

763 

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

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

765 
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

766 

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

767 

13158  768 
*** HOL *** 
769 

13899  770 
* arith(_tac) 
771 

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

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

774 
of quantifierfree linear arithmetic. 

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

776 

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

778 

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

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

14731  781 
Presburger arithmetic can also be called explicitly via presburger(_tac). 
13899  782 

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

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

785 

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

787 
are distributed over a sum of terms; 

788 

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

14731  791 
"<=", "<" and "="). 
792 

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

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

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

798 

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

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

800 
Finite_Set); 
13492  801 

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

804 

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

807 

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

810 
of the empty set. 

811 

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

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

815 
Univariate Polynomials). Contributions welcome; 

13960  816 

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

818 

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

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

822 

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

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

824 

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

826 
Fleuriot); 
13960  827 

13549  828 
* Real/HahnBanach: updated and adapted to locales; 
829 

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

13872  832 

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

834 

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

837 

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

840 
classes, interfaces, objects,virtual methods, static methods, 

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

842 
assignment, exceptions. 

13549  843 

14011  844 

13549  845 
*** ZF *** 
846 

15154  847 
* ZF/Constructible: consistency proof for AC (Gdel's constructible 
13549  848 
universe, etc.); 
849 

13872  850 
* Main ZF: virtually all theories converted to newstyle format; 
13518  851 

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

852 

13478  853 
*** ML *** 
854 

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

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

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

858 

859 
* Pure: improved error reporting of simprocs; 

860 

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

862 
up simprocs; 

863 

864 

13953  865 
*** Document preparation *** 
866 

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

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

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

870 

14731  871 
* minimized dependencies of isabelle.sty and isabellesym.sty on 
13953  872 
other packages 
873 

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

875 
broke \Rightarrow) 

876 

14731  877 
* normal size for \<zero>...\<nine> (uses \mathbf instead of 
13954  878 
textcomp package) 
13953  879 

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

880 

14572  881 

12984  882 
New in Isabelle2002 (March 2002) 
883 
 

11474  884 

11572  885 
*** Document preparation *** 
886 

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

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

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

889 
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

890 
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

891 
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

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

893 

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

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

895 
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

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

897 

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

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

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

900 

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

903 

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

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

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

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

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

912 
isatool document copies the Isabelle style files to the target 

913 
location; 

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

914 

11572  915 

11633  916 
*** Isar *** 
917 

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

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

921 
 'induct' method divinates rule instantiation from the inductive 

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

923 
instantiation of cases; 

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

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

926 
rules without further ado; 

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

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

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

930 
statement becomes is included in the hypothesis, avoiding the 

931 
slightly cumbersome show "PROP ?case" form; 

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

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

934 
rules stemming from inductive sets to be applied in unstructured 

935 
scripts, while still benefitting from proper handling of nonatomic 

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

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

938 
 'induct' proper support for mutual induction involving nonatomic 

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

940 
below); 

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

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

943 
 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

944 
 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

945 
 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

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

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

948 
 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

949 

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

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

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

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

953 
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

954 
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

955 
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

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

957 

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

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

959 

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

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

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

962 

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

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

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

969 
some examples; 

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

970 

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

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

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

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

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

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

976 

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

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

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

981 
the context elements being discharged in the obvious way; 

982 

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

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

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

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

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

988 

11722  989 
* Pure: renamed "antecedent" case to "rule_context"; 
990 

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

993 
use hardwired "Trueprop"; 

994 

11738  995 
* Pure: added 'corollary' command; 
996 

11722  997 
* Pure: fixed 'token_translation' command; 
998 

11899  999 
* Pure: removed obsolete 'exported' attribute; 
1000 

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

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

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

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

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

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

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

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

1010 

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

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

1012 
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

1013 
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

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

1015 

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

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

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

1018 

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

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

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

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

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

1023 

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

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

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

1026 

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

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

1028 
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

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

1030 

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

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

1032 
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

1033 
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

1034 

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

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

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

1037 
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

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

1039 
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

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

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

1042 

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

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

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

1045 

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

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

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

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

1049 

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

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

1051 

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

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

1057 

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

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

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

1060 

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

1061 

11474  1062 
*** HOL *** 
1063 

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

1066 

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

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

1069 

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

1071 
binary representation internally; 

1072 

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

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

1075 

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

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

1077 
are some hints on converting existing sources: 
11702  1078 

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

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

1081 
to be spaced properly; 

1082 

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

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

1085 

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

1087 

1088 
 remove all special provisions on numerals in proofs; 

1089 

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

12736  1093 
* HOL: symbolic syntax for x^2 (numeral 2); 
1094 

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

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

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

1097 
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

1098 
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

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

1100 

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

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

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

1105 
declared as simp by default; 

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

1106 
 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

1107 
qualified)  potential INCOMPATIBILITY; 
12280  1108 
 removed "make_scheme" operations (use "make" with "extend")  
1109 
INCOMPATIBILITY; 

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

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

1116 

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

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

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

1119 
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

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

1121 

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

13824  1124 
* HOL: consolidated and renamed several theories. In particular: 
14731  1125 
Ord.thy has been absorbed into HOL.thy 
1126 
String.thy has been absorbed into List.thy 

1127 

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

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

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

1130 

11657  1131 
* HOL: linorder_less_split superseded by linorder_cases; 
1132 

12917  1133 
* HOL/List: "nodups" renamed to "distinct"; 
12889  1134 

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

11437  1138 

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

1141 

1142 
delSWrapper "split_all_tac" 

1143 
addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac) 

1144 

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

11474  1146 
MAY FAIL; 
11361  1147 

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

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

1151 
necessary to attach explicit type constraints; 

11307  1152 

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

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

12489  1156 

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

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

1158 
expressions; 
11474  1159 

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

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

1161 
of "lam"  INCOMPATIBILITY; 
11474  1162 

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

1165 
renamed "Product_Type.unit"; 

11611  1166 

12564  1167 
* HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl 
1168 

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

1171 

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

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

1174 

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

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

1176 
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

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

1178 

12734  1179 
* HOLReal: added Complex_Numbers (by Gertrud Bauer); 
1180 

12690  1181 
* HOLHyperreal is now a logic image; 
1182 

11611  1183 

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

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

1185 

12622  1186 
* Isar: consts/constdefs supports mixfix syntax for continuous 
1187 
operations; 

1188 

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

1190 
HOLCF/ex/Dnat.thy; 

1191 

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

12280  1193 
potential INCOMPATIBILITY; now use plain induct_tac instead of former 
1194 
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

1195 

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

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

1197 

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

1198 

11474  1199 
*** ZF *** 
1200 

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

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

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

1205 

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

1207 
your theory on Main_ZFC; 

1208 

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

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

12563  1211 

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

1214 

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

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

1217 

12280  1218 
* 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

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

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

1221 

13025  1222 
* ZF: many new theorems about lists, ordinals, etc.; 
12850  1223 

11474  1224 

1225 
*** General *** 

1226 

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

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

1230 
also ref manual for further ML interfaces; 

1231 

1232 
* Pure/axclass: removed obsolete ML interface 

1233 
goal_subclass/goal_arity; 

1234 

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

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

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

1238 
properly; 

1239 

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

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

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

1242 

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

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

1244 
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

1245 
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

1246 
type variable); 
12280  1247 

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

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

1250 
"type_brackets"; 

1251 

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

11817  1253 
tokens into AST constants; 
11474  1254 

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

1257 
multiple declarations for same syntax element constant; 

1258 

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

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

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

1261 

12280  1262 
* Provers/classical: renamed addaltern to addafter, addSaltern to 
1263 
addSafter; 

1264 

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

1266 
as well; 

12253  1267 

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

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

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

1272 
support requires further installations, e.g. from 

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

1274 

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

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

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

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

1279 

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

1282 

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

1285 
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

1286 

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

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

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

11551  1292 

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

1295 
isolatin characters may now be used; the related isatools 

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

1297 

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

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

1300 
terminal); 

1301 

11314  1302 

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

1303 

11062  1304 
New in Isabelle992 (February 2001) 
1305 
 

1306 

10224  1307 
*** Overview of INCOMPATIBILITIES *** 
1308 

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

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

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

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

1314 
but only as far as specified by the introductions given; the old 
11130  1315 
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

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

1317 

10998  1318 
* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, 
1319 
gfp_Tarski to gfp_unfold; 

10224  1320 

10288  1321 
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; 
1322 

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

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

10793  1326 

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

1329 

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

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

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

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

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

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

1337 

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

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

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

1340 

10224  1341 

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

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

1343 

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

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

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

1348 
typewriter); 

1349 

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

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

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

1352 

10858  1353 
* some more standard symbols; see Appendix A of the system manual for 
11062  1354 
the complete list of symbols defined in isabellesym.sty; 
10858  1355 

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

1358 
definitions); 

1359 

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

1362 
actual humanreadable proof documents. Please do not include goal 

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

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

1364 

11062  1365 
* proper indentation of antiquoted output with proportional LaTeX 
1366 
fonts; 

10862  1367 

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

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

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

1370 

11062  1371 
* isatool unsymbolize tunes sources for plain ASCII communication; 
1372 

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

1373 

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

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

1375 

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

1378 
documents, due to unpredictable outcome and noncompositional proof 

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

1380 
for Prologstyle synthesis of proven results; 

1381 

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

1384 

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

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

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

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

1389 

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

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

1392 

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

1394 
statements as well; 

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

1395 

11097  1396 
* Pure: more robust selection of calculational rules; 
1397 

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

1400 

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

1402 
lemmas, using the graph browser tool; 

1403 

10944  1404 
* Pure: predict failure of "show" in interactive mode; 
1405 

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

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

1407 

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

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

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

1410 

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

1414 

10858  1415 
* HOL: local contexts (aka cases) may now contain term bindings as 
1416 
well; the 'c 