author  wenzelm 
Sun, 05 Jun 2005 11:31:14 +0200  
changeset 16251  121dc80d120a 
parent 16234  421c3522f160 
child 16373  9d020423093b 
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 

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

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

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

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

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

460 

16234  461 

462 
*** System *** 

463 

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

465 
isabelle, isatool etc.). 

466 

467 
* ISABELLE_DOC_FORMAT setting specifies preferred document format (for 

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

469 

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

471 
used by Isabelle; default is ROOT.ML. 

472 

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

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

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

475 

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

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

15703  479 

480 

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

481 

14606  482 
New in Isabelle2004 (April 2004) 
483 
 

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

484 

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

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

486 

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

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

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

489 

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

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

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

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

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

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

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

499 
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

500 

14237  501 
* Pure: Macintosh and Windows linebreaks are now allowed in theory files. 
502 

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

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

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

14233  507 

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

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

14333  512 

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

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

516 

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

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

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

14224  521 
rather than definitionally, such as the metalogic connectives. 
522 

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

525 

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

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

530 

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

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

532 

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

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

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

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

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

537 
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

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

539 
 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

540 
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

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

542 

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

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

544 
 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

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

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

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

548 

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

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

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

551 
and derived forms. 
14283  552 

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

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

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

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

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

557 
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

558 
 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

559 
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

560 
 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

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

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

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

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

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

569 
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

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

573 
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

574 

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

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

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

577 

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

578 

14136  579 
*** HOL *** 
580 

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

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

584 
can be used like any other Isabelle image. See 

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

586 

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

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

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

589 
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

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

591 
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

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

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

594 
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

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

596 

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

600 
* Numerics: 

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

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

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

14389  608 

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

14255  611 
* Records: 
612 
 Record types are now by default printed with their type abbreviation 

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

614 
the reference "print_record_type_abbr". 

14731  615 
 Simproc "record_upd_simproc" for simplification of multiple updates added 
14255  616 
(not enabled by default). 
14427  617 
 Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. 
618 
EX x. x = sel r to True (not enabled by default). 

14255  619 
 Tactic "record_split_simp_tac" to split and simplify records added. 
14731  620 

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

14136  624 

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

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

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

628 

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

14731  632 
* HOLMatrix: a first theory for matrices in HOL with an application of 
14610  633 
matrix theory to linear programming. 
14136  634 

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

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

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

14380  640 

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

14418  644 
like in normal math, and corresponding versions for < and for intersection. 
645 

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

648 

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

14380  651 

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

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

655 

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

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

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

660 
for examples. 

14464  661 

14606  662 

14536  663 
*** HOLCF *** 
664 

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

666 

14572  667 

668 

14136  669 
New in Isabelle2003 (May 2003) 
14606  670 
 
14136  671 

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

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

673 

13618  674 
* Provers/simplifier: 
675 

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

679 
the order of assumptions. 

680 

681 
Potential INCOMPATIBILITY: 

682 

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

13618  685 

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

687 

13781  688 
now gives rise to the infinite reduction sequence 
689 

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

691 

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

693 
kind of problem. 

694 

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

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

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

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

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

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

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

13618  702 

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

704 

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

707 
conditions before applying the rewrite rule): 

708 
ML "simp_depth_limit := n" 

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

710 
the simplifier would diverge. 

711 

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

712 
 Accepts free variables as head terms in congruence rules. Useful in Isar. 
13829  713 

13938  714 
 No longer aborts on failed congruence proof. Instead, the 
715 
congruence is ignored. 

716 

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

719 
as HOL/Extraction for some case studies. 

720 

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

723 
PG menu: Isabelle/Isar > Settings > Show Main Goal 
13815  724 
(ML: Proof.show_main_goal). 
725 

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

727 
rules whose conclusion matches subgoal 1: 

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

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

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

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

732 
(ML: ProofGeneral.print_intros()) 

733 

734 
* Pure: New flag trace_unify_fail causes unification to print 

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

737 
assumption failed. 

738 

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

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

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

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

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

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

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

746 

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

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

748 
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

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

750 

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

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

752 
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

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

756 
be given (the default is 40); 

757 

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

759 
(batchmode only); 

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

760 

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

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

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

763 
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

764 

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

767 
for slight decrease in efficiency; 

768 

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

771 

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

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

773 
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

774 

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

775 

13158  776 
*** HOL *** 
777 

13899  778 
* arith(_tac) 
779 

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

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

782 
of quantifierfree linear arithmetic. 

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

784 

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

786 

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

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

14731  789 
Presburger arithmetic can also be called explicitly via presburger(_tac). 
13899  790 

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

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

793 

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

795 
are distributed over a sum of terms; 

796 

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

14731  799 
"<=", "<" and "="). 
800 

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

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

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

806 

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

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

808 
Finite_Set); 
13492  809 

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

812 

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

815 

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

818 
of the empty set. 

819 

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

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

823 
Univariate Polynomials). Contributions welcome; 

13960  824 

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

826 

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

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

830 

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

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

832 

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

834 
Fleuriot); 
13960  835 

13549  836 
* Real/HahnBanach: updated and adapted to locales; 
837 

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

13872  840 

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

842 

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

845 

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

848 
classes, interfaces, objects,virtual methods, static methods, 

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

850 
assignment, exceptions. 

13549  851 

14011  852 

13549  853 
*** ZF *** 
854 

15154  855 
* ZF/Constructible: consistency proof for AC (Gdel's constructible 
13549  856 
universe, etc.); 
857 

13872  858 
* Main ZF: virtually all theories converted to newstyle format; 
13518  859 

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

860 

13478  861 
*** ML *** 
862 

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

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

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

866 

867 
* Pure: improved error reporting of simprocs; 

868 

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

870 
up simprocs; 

871 

872 

13953  873 
*** Document preparation *** 
874 

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

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

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

878 

14731  879 
* minimized dependencies of isabelle.sty and isabellesym.sty on 
13953  880 
other packages 
881 

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

883 
broke \Rightarrow) 

884 

14731  885 
* normal size for \<zero>...\<nine> (uses \mathbf instead of 
13954  886 
textcomp package) 
13953  887 

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

888 

14572  889 

12984  890 
New in Isabelle2002 (March 2002) 
891 
 

11474  892 

11572  893 
*** Document preparation *** 
894 

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

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

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

897 
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

898 
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

899 
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

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

901 

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

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

903 
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

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

905 

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

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

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

908 

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

911 

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

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

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

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

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

920 
isatool document copies the Isabelle style files to the target 

921 
location; 

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

922 

11572  923 

11633  924 
*** Isar *** 
925 

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

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

929 
 'induct' method divinates rule instantiation from the inductive 

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

931 
instantiation of cases; 

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

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

934 
rules without further ado; 

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

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

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

938 
statement becomes is included in the hypothesis, avoiding the 

939 
slightly cumbersome show "PROP ?case" form; 

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

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

942 
rules stemming from inductive sets to be applied in unstructured 

943 
scripts, while still benefitting from proper handling of nonatomic 

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

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

946 
 'induct' proper support for mutual induction involving nonatomic 

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

948 
below); 

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

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

951 
 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

952 
 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

953 
 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

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

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

956 
 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

957 

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

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

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

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

961 
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

962 
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

963 
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

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

965 

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

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

967 

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

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

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

970 

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

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

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

977 
some examples; 

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

978 

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

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

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

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

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

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

984 

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

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

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

989 
the context elements being discharged in the obvious way; 

990 

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

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

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

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

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

996 

11722  997 
* Pure: renamed "antecedent" case to "rule_context"; 
998 

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

1001 
use hardwired "Trueprop"; 

1002 

11738  1003 
* Pure: added 'corollary' command; 
1004 

11722  1005 
* Pure: fixed 'token_translation' command; 
1006 

11899  1007 
* Pure: removed obsolete 'exported' attribute; 
1008 

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

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

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

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

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

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

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

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

1018 

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

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

1020 
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

1021 
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

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

1023 

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

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

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

1026 

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

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

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

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

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

1031 

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

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

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

1034 

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

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

1036 
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

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

1038 

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

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

1040 
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

1041 
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

1042 

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

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

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

1045 
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

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

1047 
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

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

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

1050 

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

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

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

1053 

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

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

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

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

1057 

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

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

1059 

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

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

1065 

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

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

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

1068 

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

1069 

11474  1070 
*** HOL *** 
1071 

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

1074 

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

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

1077 

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

1079 
binary representation internally; 

1080 

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

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

1083 

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

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

1085 
are some hints on converting existing sources: 
11702  1086 

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

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

1089 
to be spaced properly; 

1090 

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

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

1093 

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

1095 

1096 
 remove all special provisions on numerals in proofs; 

1097 

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

12736  1101 
* HOL: symbolic syntax for x^2 (numeral 2); 
1102 

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

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

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

1105 
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

1106 
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

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

1108 

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

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

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

1113 
declared as simp by default; 

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

1114 
 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

1115 
qualified)  potential INCOMPATIBILITY; 
12280  1116 
 removed "make_scheme" operations (use "make" with "extend")  
1117 
INCOMPATIBILITY; 

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

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

1124 

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

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

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

1127 
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

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

1129 

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

13824  1132 
* HOL: consolidated and renamed several theories. In particular: 
14731  1133 
Ord.thy has been absorbed into HOL.thy 
1134 
String.thy has been absorbed into List.thy 

1135 

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

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

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

1138 

11657  1139 
* HOL: linorder_less_split superseded by linorder_cases; 
1140 

12917  1141 
* HOL/List: "nodups" renamed to "distinct"; 
12889  1142 

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

11437  1146 

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

1149 

1150 
delSWrapper "split_all_tac" 

1151 
addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac) 

1152 

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

11474  1154 
MAY FAIL; 
11361  1155 

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

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

1159 
necessary to attach explicit type constraints; 

11307  1160 

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

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

12489  1164 

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

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

1166 
expressions; 
11474  1167 

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

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

1169 
of "lam"  INCOMPATIBILITY; 
11474  1170 

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

1173 
renamed "Product_Type.unit"; 

11611  1174 

12564  1175 
* HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl 
1176 

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

1179 

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

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

1182 

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

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

1184 
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

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

1186 

12734  1187 
* HOLReal: added Complex_Numbers (by Gertrud Bauer); 
1188 

12690  1189 
* HOLHyperreal is now a logic image; 
1190 

11611  1191 

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

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

1193 

12622  1194 
* Isar: consts/constdefs supports mixfix syntax for continuous 
1195 
operations; 

1196 

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

1198 
HOLCF/ex/Dnat.thy; 

1199 

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

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

1203 

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

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

1205 

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

1206 

11474  1207 
*** ZF *** 
1208 

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

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

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

1213 

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

1215 
your theory on Main_ZFC; 

1216 

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

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

12563  1219 

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

1222 

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

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

1225 

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

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

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

1229 

13025  1230 
* ZF: many new theorems about lists, ordinals, etc.; 
12850  1231 

11474  1232 

1233 
*** General *** 

1234 

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

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

1238 
also ref manual for further ML interfaces; 

1239 

1240 
* Pure/axclass: removed obsolete ML interface 

1241 
goal_subclass/goal_arity; 

1242 

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

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

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

1246 
properly; 

1247 

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

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

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

1250 

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

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

1252 
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

1253 
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

1254 
type variable); 
12280  1255 

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

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

1258 
"type_brackets"; 

1259 

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

11817  1261 
tokens into AST constants; 
11474  1262 

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

1265 
multiple declarations for same syntax element constant; 

1266 

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

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

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

1269 

12280  1270 
* Provers/classical: renamed addaltern to addafter, addSaltern to 
1271 
addSafter; 

1272 

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

1274 
as well; 

12253  1275 

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

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

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

1280 
support requires further installations, e.g. from 

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

1282 

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

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

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

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

1287 

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

1290 

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

1293 
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

1294 

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

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

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

11551  1300 

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

1303 
isolatin characters may now be used; the related isatools 

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

1305 

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

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

1308 
terminal); 

1309 

11314  1310 

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

1311 

11062  1312 
New in Isabelle992 (February 2001) 
1313 
 

1314 

10224  1315 
*** Overview of INCOMPATIBILITIES *** 
1316 

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

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

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

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

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

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

1325 

10998  1326 
* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, 
1327 
gfp_Tarski to gfp_unfold; 

10224  1328 

10288  1329 
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; 
1330 

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

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

10793  1334 

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

1337 

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

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

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

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

1343 
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

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

1345 

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

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

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

1348 

10224  1349 

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

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

1351 

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

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

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

1356 
typewriter); 

1357 

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

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

1359 
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

1360 

10858  1361 
* some more standard symbols; see Appendix A of the system manual for 
11062  1362 
the complete list of symbols defined in isabellesym.sty; 
10858  1363 

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

1366 
definitions); 

1367 

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

1370 
actual humanreadable proof documents. Please do not include goal 

1371 
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

1372 

11062  1373 
* proper indentation of antiquoted output with proportional LaTeX 
1374 
fonts; 

10862  1375 

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

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

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

1378 

11062  1379 
* isatool unsymbolize tunes sources for plain ASCII communication; 
1380 

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

1381 

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

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

1383 

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

1386 
documents, due to unpredictable outcome and noncompositional proof 

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

1388 
for Prologstyle synthesis of proven results; 

1389 

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

1392 

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

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

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

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

1397 

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

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

1400 

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

1402 
statements as well; 

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

1403 

11097  1404 
* Pure: more robust selection of calculational rules; 
1405 

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

1408 

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

1410 
lemmas, using the graph browser tool; 

1411 

10944  1412 
* Pure: predict failure of "show" in interactive mode; 
1413 

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

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

1415 

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

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

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

1418 

10557  1419 
* HOL: cases and induct rules now provide explicit hints about the 