author  wenzelm 
Fri, 16 Apr 2004 21:00:36 +0200  
changeset 14607  099575a938e5 
parent 14606  0be6c11e7128 
child 14610  9c2e31e483b2 
permissions  rwrr 
5363  1 
Isabelle NEWS  history userrelevant changes 
2 
============================================== 

2553  3 

14606  4 
New in Isabelle2004 (April 2004) 
5 
 

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

6 

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

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

8 

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

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

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

11 

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

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

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

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

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

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

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

21 
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

22 

14237  23 
* Pure: Macintosh and Windows linebreaks are now allowed in theory files. 
24 

14234
9590df3c5f2a
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
kleing
parents:
14233
diff
changeset

25 
* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
14606  26 
allowed in identifiers. Similar to Greek letters \<^isub> is now considered 
14234
9590df3c5f2a
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
kleing
parents:
14233
diff
changeset

27 
a normal (but invisible) letter. For multiple letter subscripts repeat 
9590df3c5f2a
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
kleing
parents:
14233
diff
changeset

28 
\<^isub> like this: x\<^isub>1\<^isub>2. 
14233  29 

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

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

14333  34 

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

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

38 

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

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

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

14224  43 
rather than definitionally, such as the metalogic connectives. 
44 

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

47 

14547  48 
* Presentation: generated HTML now uses a CSS style sheet to make layout 
14606  49 
(somewhat) independent of content. It is copied from lib/html/isabelle.css. 
14547  50 
It can be changed to alter the colors/layout of generated pages. 
51 

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

52 

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

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

54 

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

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

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

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

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

59 
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

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

61 
 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

62 
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

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

64 

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

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

66 
 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

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

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

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

70 

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

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

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

73 
and derived forms. 
14283  74 

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

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

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

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

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

79 
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

80 
 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

81 
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

82 
 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

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

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

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

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

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

91 
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

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

95 
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

96 

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

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

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

99 

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

100 

14136  101 
*** HOL *** 
102 

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

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

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

105 
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

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

107 
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

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

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

110 
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

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

112 

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

115 

116 
* Numerics: 

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

118 
now formalized using the Ring_and_Field theory mentioned above. 

119 
 INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently 

120 
than before, because now they are set up once in a generic manner. 

14480  121 
 INCOMPATIBILITY: many typespecific arithmetic laws have gone. 
122 
Look for the general versions in Ring_and_Field (and Power if they concern 

123 
exponentiation). 

14389  124 

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

14255  127 
* Records: 
128 
 Record types are now by default printed with their type abbreviation 

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

130 
the reference "print_record_type_abbr". 

131 
 Simproc "record_upd_simproc" for simplification of multiple updates added 

132 
(not enabled by default). 

14427  133 
 Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp. 
134 
EX x. x = sel r to True (not enabled by default). 

14255  135 
 Tactic "record_split_simp_tac" to split and simplify records added. 
136 

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

14136  140 

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

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

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

144 

14243  145 
* HOLex: InductiveInvariant_examples illustrates advanced recursive function 
146 
defintions, thanks to Sava Krsti\'{c} and John Matthews. 

14136  147 

14380  148 
* Unions and Intersections: 
149 
The xsymbol output syntax of UN and INT has been changed 

150 
from "\<Union>x \<in> A. B" to "\<Union\<^bsub>x \<in> A\<^esub> B" 

151 
i.e. the index formulae has become a subscript, like in normal math. 

152 
Similarly for "\<Union>x. B", and for \<Inter> instead of \<Union>. 

153 
The subscript version is also accepted as input syntax. 

154 

14418  155 
* Unions and Intersections over Intervals: 
156 
There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is 

157 
also an xsymbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" 

158 
like in normal math, and corresponding versions for < and for intersection. 

159 

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

14380  162 

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

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

166 

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

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

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

171 
for examples. 

14464  172 

14606  173 

14536  174 
*** HOLCF *** 
175 

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

177 

14572  178 

179 

14136  180 
New in Isabelle2003 (May 2003) 
14606  181 
 
14136  182 

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

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

184 

13618  185 
* Provers/simplifier: 
186 

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

190 
the order of assumptions. 

191 

192 
Potential INCOMPATIBILITY: 

193 

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

13618  196 

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

198 

13781  199 
now gives rise to the infinite reduction sequence 
200 

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

202 

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

204 
kind of problem. 

205 

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

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

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

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

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

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

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

13618  213 

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

215 

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

218 
conditions before applying the rewrite rule): 

219 
ML "simp_depth_limit := n" 

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

221 
the simplifier would diverge. 

222 

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

223 
 Accepts free variables as head terms in congruence rules. Useful in Isar. 
13829  224 

13938  225 
 No longer aborts on failed congruence proof. Instead, the 
226 
congruence is ignored. 

227 

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

230 
as HOL/Extraction for some case studies. 

231 

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

234 
PG menu: Isabelle/Isar > Settings > Show Main Goal 
13815  235 
(ML: Proof.show_main_goal). 
236 

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

238 
rules whose conclusion matches subgoal 1: 

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

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

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

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

243 
(ML: ProofGeneral.print_intros()) 

244 

245 
* Pure: New flag trace_unify_fail causes unification to print 

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

248 
assumption failed. 

249 

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

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

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

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

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

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

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

257 

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

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

259 
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

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

261 

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

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

263 
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

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

267 
be given (the default is 40); 

268 

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

270 
(batchmode only); 

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

271 

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

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

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

274 
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

275 

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

278 
for slight decrease in efficiency; 

279 

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

282 

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

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

284 
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

285 

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

286 

13158  287 
*** HOL *** 
288 

13899  289 
* arith(_tac) 
290 

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

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

293 
of quantifierfree linear arithmetic. 

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

295 

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

297 

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

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

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

301 

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

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

304 

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

306 
are distributed over a sum of terms; 

307 

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

310 
"<=", "<" and "="). 

311 

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

314 

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

317 

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

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

319 
Finite_Set); 
13492  320 

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

323 

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

326 

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

329 
of the empty set. 

330 

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

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

334 
Univariate Polynomials). Contributions welcome; 

13960  335 

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

337 

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

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

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

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

341 

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

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

343 

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

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

345 
Fleuriot); 
13960  346 

13549  347 
* Real/HahnBanach: updated and adapted to locales; 
348 

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

13872  351 

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

353 

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

356 

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

359 
classes, interfaces, objects,virtual methods, static methods, 

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

361 
assignment, exceptions. 

13549  362 

14011  363 

13549  364 
*** ZF *** 
365 

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

367 
universe, etc.); 

368 

13872  369 
* Main ZF: virtually all theories converted to newstyle format; 
13518  370 

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

371 

13478  372 
*** ML *** 
373 

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

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

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

377 

378 
* Pure: improved error reporting of simprocs; 

379 

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

381 
up simprocs; 

382 

383 

13953  384 
*** Document preparation *** 
385 

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

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

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

389 

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

391 
other packages 

392 

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

394 
broke \Rightarrow) 

395 

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

13953  398 

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

399 

14572  400 

12984  401 
New in Isabelle2002 (March 2002) 
402 
 

11474  403 

11572  404 
*** Document preparation *** 
405 

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

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

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

408 
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

409 
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

410 
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

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

412 

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

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

414 
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

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

416 

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

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

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

419 

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

422 

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

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

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

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

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

431 
isatool document copies the Isabelle style files to the target 

432 
location; 

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

433 

11572  434 

11633  435 
*** Isar *** 
436 

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

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

440 
 'induct' method divinates rule instantiation from the inductive 

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

442 
instantiation of cases; 

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

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

445 
rules without further ado; 

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

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

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

449 
statement becomes is included in the hypothesis, avoiding the 

450 
slightly cumbersome show "PROP ?case" form; 

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

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

453 
rules stemming from inductive sets to be applied in unstructured 

454 
scripts, while still benefitting from proper handling of nonatomic 

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

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

457 
 'induct' proper support for mutual induction involving nonatomic 

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

459 
below); 

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

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

462 
 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

463 
 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

464 
 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

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

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

467 
 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

468 

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

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

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

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

472 
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

473 
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

474 
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

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

476 

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

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

478 

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

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

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

481 

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

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

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

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

488 
some examples; 

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

489 

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

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

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

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

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

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

495 

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

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

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

500 
the context elements being discharged in the obvious way; 

501 

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

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

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

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

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

507 

11722  508 
* Pure: renamed "antecedent" case to "rule_context"; 
509 

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

512 
use hardwired "Trueprop"; 

513 

11738  514 
* Pure: added 'corollary' command; 
515 

11722  516 
* Pure: fixed 'token_translation' command; 
517 

11899  518 
* Pure: removed obsolete 'exported' attribute; 
519 

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

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

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

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

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

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

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

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

529 

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

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

531 
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

532 
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

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

534 

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

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

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

537 

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

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

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

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

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

542 

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

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

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

545 

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

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

547 
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

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

549 

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

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

551 
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

552 
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

553 

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

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

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

556 
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

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

558 
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

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

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

561 

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

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

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

564 

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

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

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

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

568 

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

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

570 

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

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

576 

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

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

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

579 

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

580 

11474  581 
*** HOL *** 
582 

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

585 

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

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

588 

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

590 
binary representation internally; 

591 

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

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

594 

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

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

596 
are some hints on converting existing sources: 
11702  597 

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

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

600 
to be spaced properly; 

601 

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

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

604 

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

606 

607 
 remove all special provisions on numerals in proofs; 

608 

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

12736  612 
* HOL: symbolic syntax for x^2 (numeral 2); 
613 

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

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

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

616 
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

617 
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

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

619 

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

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

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

624 
declared as simp by default; 

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

625 
 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

626 
qualified)  potential INCOMPATIBILITY; 
12280  627 
 removed "make_scheme" operations (use "make" with "extend")  
628 
INCOMPATIBILITY; 

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

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

635 

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

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

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

638 
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

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

640 

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

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

645 
String.thy has been absorbed into List.thy 

646 

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

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

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

649 

11657  650 
* HOL: linorder_less_split superseded by linorder_cases; 
651 

12917  652 
* HOL/List: "nodups" renamed to "distinct"; 
12889  653 

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

11437  657 

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

660 

661 
delSWrapper "split_all_tac" 

662 
addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac) 

663 

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

11474  665 
MAY FAIL; 
11361  666 

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

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

670 
necessary to attach explicit type constraints; 

11307  671 

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

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

12489  675 

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

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

677 
expressions; 
11474  678 

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

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

680 
of "lam"  INCOMPATIBILITY; 
11474  681 

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

684 
renamed "Product_Type.unit"; 

11611  685 

12564  686 
* HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl 
687 

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

690 

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

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

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

693 

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

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

695 
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

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

697 

12734  698 
* HOLReal: added Complex_Numbers (by Gertrud Bauer); 
699 

12690  700 
* HOLHyperreal is now a logic image; 
701 

11611  702 

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

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

704 

12622  705 
* Isar: consts/constdefs supports mixfix syntax for continuous 
706 
operations; 

707 

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

709 
HOLCF/ex/Dnat.thy; 

710 

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

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

714 

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

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

716 

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

717 

11474  718 
*** ZF *** 
719 

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

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

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

724 

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

726 
your theory on Main_ZFC; 

727 

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

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

12563  730 

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

733 

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

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

736 

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

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

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

740 

13025  741 
* ZF: many new theorems about lists, ordinals, etc.; 
12850  742 

11474  743 

744 
*** General *** 

745 

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

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

749 
also ref manual for further ML interfaces; 

750 

751 
* Pure/axclass: removed obsolete ML interface 

752 
goal_subclass/goal_arity; 

753 

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

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

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

757 
properly; 

758 

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

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

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

761 

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

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

763 
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

764 
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

765 
type variable); 
12280  766 

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

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

769 
"type_brackets"; 

770 

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

11817  772 
tokens into AST constants; 
11474  773 

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

776 
multiple declarations for same syntax element constant; 

777 

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

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

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

780 

12280  781 
* Provers/classical: renamed addaltern to addafter, addSaltern to 
782 
addSafter; 

783 

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

785 
as well; 

12253  786 

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

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

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

791 
support requires further installations, e.g. from 

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

793 

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

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

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

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

798 

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

801 

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

804 
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

805 

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

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

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

11551  811 

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

814 
isolatin characters may now be used; the related isatools 

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

816 

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

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

819 
terminal); 

820 

11314  821 

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

822 

11062  823 
New in Isabelle992 (February 2001) 
824 
 

825 

10224  826 
*** Overview of INCOMPATIBILITIES *** 
827 

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

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

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

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

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

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

836 

10998  837 
* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, 
838 
gfp_Tarski to gfp_unfold; 

10224  839 

10288  840 
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; 
841 

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

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

10793  845 

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

848 

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

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

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

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

854 
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

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

856 

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

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

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

859 

10224  860 

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

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

862 

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

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

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

867 
typewriter); 

868 

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

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

870 
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

871 

10858  872 
* some more standard symbols; see Appendix A of the system manual for 
11062  873 
the complete list of symbols defined in isabellesym.sty; 
10858  874 

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

877 
definitions); 

878 

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

881 
actual humanreadable proof documents. Please do not include goal 

882 
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

883 

11062  884 
* proper indentation of antiquoted output with proportional LaTeX 
885 
fonts; 

10862  886 

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

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

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

889 

11062  890 
* isatool unsymbolize tunes sources for plain ASCII communication; 
891 

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

892 

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

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

894 

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

897 
documents, due to unpredictable outcome and noncompositional proof 

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

899 
for Prologstyle synthesis of proven results; 

900 

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

903 

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

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

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

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

908 

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

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

911 

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

913 
statements as well; 

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

914 

11097  915 
* Pure: more robust selection of calculational rules; 
916 

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

919 

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

921 
lemmas, using the graph browser tool; 

922 

10944  923 
* Pure: predict failure of "show" in interactive mode; 
924 

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

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

926 

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

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

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

929 

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

933 

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

936 
the result to be shown in each case; 

937 

10770  938 
* HOL: added 'recdef_tc' command; 
939 

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

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

941 

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

942 

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

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

944 

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

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

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

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

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

950 

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

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

954 

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

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

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

959 
literature; 

960 

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

964 

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

967 

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

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

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

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

971 

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

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

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

974 

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

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

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

977 

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

980 
functions for the reals; 

10756  981 

11094  982 
* HOL/Real, HOL/Hyperreal: improved arithmetic simplification; 
10391  983 

10858  984 

10474  985 
*** CTT *** 
986 

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

10474  989 

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

992 

10474  993 

10391  994 
*** General *** 
995 

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

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

999 
the Isabelle inference kernel has been greatly improved; 

1000 

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

1003 

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

1006 

11124  1007 
* system: support Poly/ML 4.0; 
1008 

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

1010 

10391  1011 

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

1012 

10103  1013 
New in Isabelle991 (October 2000) 
1014 
 

8015  1015 

10003  1016 
*** Overview of INCOMPATIBILITIES *** 
8014  1017 

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

1020 
issue the following ML commands: 

1021 

1022 
Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; 

1023 
Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; 

8788  1024 

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

10003  1027 

1028 
* HOL: nat_less_induct renamed to less_induct; 

1029 

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

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

8967  1032 

10003  1033 
select_equality > some_equality 
1034 
select_eq_Ex > some_eq_ex 

1035 
selectI2EX > someI2_ex 

1036 
selectI2 > someI2 

1037 
selectI > someI 

1038 
select1_equality > some1_equality 

1039 
Eps_sym_eq > some_sym_eq_trivial 

1040 
Eps_eq > some_eq_trivial 

1041 

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

1043 

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

1045 
instead); 

1046 

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

1048 
f.simps instead of f.rules; 

1049 

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

1051 

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

1053 
sometimes be needed; 

1054 

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

8014  1056 

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

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

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

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

1061 
now "<*lex*>" instead of "**"; 
8705  1062 

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

9971  1065 

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

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

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

1068 

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

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

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

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

1072 

8848  1073 
* HOL/Real: "rabs" replaced by overloaded "abs" function; 
1074 

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

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

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

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

1078 

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

9908  1081 

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

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

1084 

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

9542  1087 

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

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

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

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

1092 

9612  1093 
* Isar/HOL: renamed "intrs" to "intros" in inductive definitions; 
1094 

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

1095 
* Provers: strengthened force_tac by using new first_best_tac; 
9402  1096 

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

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

1099 

8014  1100 

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

1102 

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

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

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

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

1107 

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

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

1110 

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

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

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

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

1114 

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

8566  1118 

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

1120 

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

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

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

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

1124 

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

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

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

1128 

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

1129 

8184  1130 
*** Isar *** 
1131 

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

1134 
accommodates incremental typeinference very nicely; 

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

1135 

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

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

1138 

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

1141 
useful to collect intermediate results without explicit name 

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

1143 
premises; 

8184  1144 

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

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

1148 
to theorems as "tags"; 

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

1149 

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

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

1152 

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

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

1155 

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

1157 

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

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

1160 

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

1163 
with the version in Provers/classical; 

9612  1164 

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

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

1167 

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

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

1170 

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

9612  1173 

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

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

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

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

1178 

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

1181 

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

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

1184 
well (including splits); 

1185 

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

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

1188 

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

1190 
of Simplifier and Classical reasoner); 

1191 

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

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

1194 
recdef) support case names and properly name parameters; 

9612  1195 

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

1198 
calculations; 

1199 

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

1201 
method anyway; 

1202 

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

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

1205 
foo.split foo.split_asm for each datatype; 

1206 

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

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

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

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

1211 

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

1213 

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

1215 

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

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

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

1218 
proof states; 
8487  1219 

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

8487  1223 

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

1227 
(for HOL datatypes); 

8534  1228 

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

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

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

1232 

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

1234 

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

1237 
(print_commands, print_methods etc.); 

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

1238 

10003  1239 
* Isar: added 'nothing'  the empty list of theorems; 
9239  1240 

8184  1241 

8014  1242 
*** HOL *** 
1243 

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

1246 
verifier and a lightweight bytecode verifier, including proofs of 

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

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

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

1250 

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

8014  1253 

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

1254 
* HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese 
10003  1255 
Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M 
1256 
Rasmussen; 

8570  1257 

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

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

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

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

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

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

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

1264 

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

9542  1267 

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

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

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

1270 

10003  1271 
* HOL/Lambda: converted into newstyle theory and document; 
9542  1272 

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

1275 
representation; very useful in avoiding lifting of operations; 

8848  1276 

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

1279 
well; admit "r" as field name; 

9542  1280 

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

1283 

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

1285 
Types nat and int belong to this axclass; 

1286 

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

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

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

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

8736  1294 

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

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

9835  1298 

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

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

1302 

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

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

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

8603  1308 

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

1311 
termination conditions are proved automatically, these simplification 

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

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

1314 
each equation; 

1315 

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

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

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

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

1319 
invariant proof rule for while is applied. 
9457  1320 

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

8925  1323 

8848  1324 
* HOL: theorems impI, allI, ballI bound as "strip"; 
1325 

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

1329 

10003  1330 
* HOL/Real: "rabs" replaced by overloaded "abs" function; 
9737  1331 

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

8626  1334 

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

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

1337 

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

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

1341 
bogus); 

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

1342 

8412  1343 

9542  1344 
*** ZF *** 
1345 

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

9542  1348 

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

1351 
making the algebraic laws unconditional; 

9542  1352 

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

9542  1355 

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

9542  1358 

10003  1359 
* ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic 
1360 
simplification; 

9388  1361 

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

9388  1364 

1365 

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

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

1367 

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

1370 

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

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

1373 

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

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

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

1376 

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

1379 
use instead the strong form, 

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

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

1382 
from destructrules; 

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

1383 

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

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

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

1386 

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

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

1388 

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

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

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

1391 

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

1394 
situations; 

1395 

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

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

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

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

1399 

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

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

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

1402 

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

1403 
* system: provide TAGS file for Isabelle sources; 
9052  1404 

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

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

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

1407 

8994
