wenzelm@2553

1 

wenzelm@2553

2 
Isabelle NEWS  history of uservisible changes

wenzelm@2553

3 
================================================

wenzelm@2553

4 

wenzelm@3006

5 
New in Isabelle948 (May 1997)

wenzelm@3006

6 


wenzelm@2654

7 

paulson@3002

8 
*** General Changes ***

paulson@3002

9 

paulson@3002

10 
* new utilities to build / run / maintain Isabelle etc. (in parts

paulson@3002

11 
still somewhat experimental); old Makefiles etc. still functional;

wenzelm@2971

12 

wenzelm@2825

13 
* INSTALL text, together with ./configure and ./build scripts;

wenzelm@2773

14 

wenzelm@3006

15 
* reimplemented type inference for greater efficiency, better error

wenzelm@3006

16 
messages and clean internal interface;

paulson@3002

17 

paulson@3002

18 
* prlim command for dealing with lots of subgoals (an easier way of

paulson@3002

19 
setting goals_limit);

paulson@3002

20 

wenzelm@3006

21 

wenzelm@3006

22 
*** Syntax ***

paulson@3002

23 

paulson@3002

24 
* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to

paulson@3002

25 
be used in conjunction with the Isabelle symbol font; uses the

paulson@3002

26 
"symbols" syntax table;

paulson@3002

27 

wenzelm@2705

28 
* added token_translation interface (may translate name tokens in

wenzelm@2756

29 
arbitrary ways, dependent on their type (free, bound, tfree, ...) and

wenzelm@2756

30 
the current print_mode);

wenzelm@2705

31 

wenzelm@2730

32 
* token translations for modes "xterm" and "xterm_color" that display

wenzelm@3006

33 
names in bold, underline etc. or colors (which requires a color

wenzelm@3006

34 
version of xterm);

wenzelm@2730

35 

paulson@3002

36 
* now supports alternative (named) syntax tables (parser and pretty

paulson@3002

37 
printer); internal interface is provided by add_modesyntax(_i);

paulson@3002

38 

paulson@3002

39 
* infixes may now be declared with names independent of their syntax;

paulson@3002

40 

paulson@3002

41 
* added typed_print_translation (like print_translation, but may

paulson@3002

42 
access type of constant);

paulson@3002

43 

wenzelm@3006

44 

paulson@3002

45 
*** Classical Reasoner ***

paulson@3002

46 

paulson@3002

47 
Blast_tac: a new tactic! It is often more powerful than fast_tac, but has

paulson@3002

48 
some limitations. Blast_tac...

paulson@3002

49 
+ ignores addss, addbefore, addafter; this restriction is intrinsic

paulson@3002

50 
+ ignores elimination rules that don't have the correct format

paulson@3002

51 
(the conclusion MUST be a formula variable)

paulson@3002

52 
+ ignores types, which can make HOL proofs fail

paulson@3002

53 
+ rules must not require higherorder unification, e.g. apply_type in ZF

paulson@3002

54 
[message "Function Var's argument not a bound variable" relates to this]

paulson@3002

55 
+ its proof strategy is more general but can actually be slower

paulson@3002

56 

paulson@3002

57 
* substitution with equality assumptions no longer permutes other assumptions.

paulson@3002

58 

paulson@3002

59 
* minor changes in semantics of addafter (now called addaltern); renamed

paulson@3002

60 
setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper

paulson@3002

61 
(and access functions for it)

paulson@3002

62 

paulson@3002

63 
* improved combination of classical reasoner and simplifier: new

paulson@3002

64 
addss, auto_tac, functions for handling clasimpsets, ... Now, the

paulson@3002

65 
simplification is safe (therefore moved to safe_step_tac) and thus

paulson@3002

66 
more complete, as multiple instantiation of unknowns (with slow_tac).

paulson@3002

67 
COULD MAKE EXISTING PROOFS FAIL; in case of problems with

paulson@3002

68 
old proofs, use unsafe_addss and unsafe_auto_tac

paulson@3002

69 

wenzelm@3006

70 

paulson@3002

71 
*** Simplifier ***

paulson@3002

72 

wenzelm@3006

73 
* added interface for simplification procedures (functions that

wenzelm@3006

74 
produce *proven* rewrite rules on the fly, depending on current

wenzelm@3006

75 
redex);

wenzelm@3006

76 

wenzelm@3006

77 
* ordering on terms as parameter (used for ordered rewriting);

wenzelm@3006

78 

paulson@3002

79 
* new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.

paulson@3002

80 

paulson@3002

81 
* the solver is now split into a safe and an unsafe part.

paulson@3002

82 
This should be invisible for the normal user, except that the

paulson@3002

83 
functions setsolver and addsolver have been renamed to setSolver and

paulson@3002

84 
addSolver. added safe_asm_full_simp_tac.

paulson@3002

85 

paulson@3002

86 

paulson@3002

87 
*** HOL ***

paulson@3002

88 

paulson@3002

89 
* patterns in case expressions allow tuple patterns as arguments to

paulson@3002

90 
constructors, for example `case x of [] => ...  (x,y,z)#ps => ...'

paulson@3002

91 

paulson@3002

92 
* primrec now also works with type nat;

paulson@3002

93 

paulson@3002

94 
* the constant for negation has been renamed from "not" to "Not" to

paulson@3002

95 
harmonize with FOL, ZF, LK, etc.

paulson@3002

96 

paulson@3002

97 
* HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists

paulson@3002

98 

paulson@3002

99 
* HOL/ex/Ring.thy declares cring_simp, which solves equational

paulson@3002

100 
problems in commutative rings, using axiomatic type classes for + and *;

paulson@3002

101 

paulson@3002

102 
* more examples in HOL/MiniML and HOL/Auth;

paulson@3002

103 

paulson@3002

104 
* more default rewrite rules for quantifiers, union/intersection;

paulson@3002

105 

slotosch@2653

106 
* HOLCF changes: derived all rules and arities

slotosch@2653

107 
+ axiomatic type classes instead of classes

slotosch@2653

108 
+ typedef instead of faking type definitions

paulson@2747

109 
+ eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.

wenzelm@2730

110 
+ new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po

slotosch@2653

111 
+ eliminated the types void, one, tr

slotosch@2653

112 
+ use unit lift and bool lift (with translations) instead of one and tr

slotosch@2653

113 
+ eliminated blift from Lift3.thy (use Def instead of blift)

paulson@2747

114 
all eliminated rules are derived as theorems > no visible changes

oheimb@2649

115 

wenzelm@3006

116 

paulson@3002

117 
*** ZF ***

wenzelm@2553

118 

paulson@2865

119 
* ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default

paulson@2865

120 
rewrite rule; this may affect some proofs. eq_cs is gone but can be put back

paulson@2865

121 
as ZF_cs addSIs [equalityI];

wenzelm@2553

122 

wenzelm@2554

123 

wenzelm@2732

124 

wenzelm@2553

125 
New in Isabelle947 (November 96)

wenzelm@2553

126 


wenzelm@2553

127 

wenzelm@2553

128 
* allowing negative levels (as offsets) in prlev and choplev;

wenzelm@2553

129 

wenzelm@2554

130 
* superlinear speedup for large simplifications;

wenzelm@2554

131 

wenzelm@2554

132 
* FOL, ZF and HOL now use miniscoping: rewriting pushes

wenzelm@2554

133 
quantifications in as far as possible (COULD MAKE EXISTING PROOFS

wenzelm@2554

134 
FAIL); can suppress it using the command Delsimps (ex_simps @

wenzelm@2554

135 
all_simps); De Morgan laws are also now included, by default;

wenzelm@2554

136 

wenzelm@2554

137 
* improved printing of ==> : ~:

wenzelm@2554

138 

wenzelm@2554

139 
* new objectlogic "Sequents" adds linear logic, while replacing LK

wenzelm@2554

140 
and Modal (thanks to Sara Kalvala);

wenzelm@2554

141 

wenzelm@2554

142 
* HOL/Auth: correctness proofs for authentication protocols;

wenzelm@2554

143 

wenzelm@2554

144 
* HOL: new auto_tac combines rewriting and classical reasoning (many

wenzelm@2554

145 
examples on HOL/Auth);

wenzelm@2554

146 

wenzelm@2554

147 
* HOL: new command AddIffs for declaring theorems of the form P=Q to

wenzelm@2554

148 
the rewriter and classical reasoner simultaneously;

wenzelm@2554

149 

wenzelm@2554

150 
* function uresult no longer returns theorems in "standard" format;

wenzelm@2554

151 
regain previous version by: val uresult = standard o uresult;

wenzelm@2554

152 

wenzelm@2554

153 

wenzelm@2554

154 

wenzelm@2554

155 
New in Isabelle946

wenzelm@2554

156 


wenzelm@2554

157 

wenzelm@2554

158 
* oracles  these establish an interface between Isabelle and trusted

wenzelm@2554

159 
external reasoners, which may deliver results as theorems;

wenzelm@2554

160 

wenzelm@2554

161 
* proof objects (in particular record all uses of oracles);

wenzelm@2554

162 

wenzelm@2554

163 
* Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;

wenzelm@2554

164 

wenzelm@2554

165 
* "constdefs" section in theory files;

wenzelm@2554

166 

wenzelm@2554

167 
* "primrec" section (HOL) no longer requires names;

wenzelm@2554

168 

wenzelm@2554

169 
* internal type "tactic" now simply "thm > thm Sequence.seq";

wenzelm@2554

170 

wenzelm@2554

171 

wenzelm@2554

172 

wenzelm@2554

173 
New in Isabelle945

wenzelm@2554

174 


wenzelm@2554

175 

wenzelm@2554

176 
* reduced space requirements;

wenzelm@2554

177 

wenzelm@2554

178 
* automatic HTML generation from theories;

wenzelm@2554

179 

wenzelm@2554

180 
* theory files no longer require "..." (quotes) around most types;

wenzelm@2554

181 

wenzelm@2554

182 
* new examples, including two proofs of the ChurchRosser theorem;

wenzelm@2554

183 

wenzelm@2554

184 
* noncurried (1994) version of HOL is no longer distributed;

wenzelm@2554

185 

wenzelm@2553

186 

paulson@2557

187 

paulson@2557

188 
New in Isabelle944

paulson@2557

189 


paulson@2557

190 

paulson@2747

191 
* greatly reduced space requirements;

paulson@2557

192 

paulson@2557

193 
* theory files (.thy) no longer require \...\ escapes at line breaks;

paulson@2557

194 

paulson@2557

195 
* searchable theorem database (see the section "Retrieving theorems" on

paulson@2557

196 
page 8 of the Reference Manual);

paulson@2557

197 

paulson@2557

198 
* new examples, including Grabczewski's monumental case study of the

paulson@2557

199 
Axiom of Choice;

paulson@2557

200 

paulson@2557

201 
* The previous version of HOL renamed to Old_HOL;

paulson@2557

202 

paulson@2557

203 
* The new version of HOL (previously called CHOL) uses a curried syntax

paulson@2557

204 
for functions. Application looks like f a b instead of f(a,b);

paulson@2557

205 

paulson@2557

206 
* Mutually recursive inductive definitions finally work in HOL;

paulson@2557

207 

paulson@2557

208 
* In ZF, patternmatching on tuples is now available in all abstractions and

paulson@2557

209 
translates to the operator "split";

paulson@2557

210 

paulson@2557

211 

paulson@2557

212 

paulson@2557

213 
New in Isabelle943

paulson@2557

214 


paulson@2557

215 

paulson@2557

216 
* new infix operator, addss, allowing the classical reasoner to

paulson@2557

217 
perform simplification at each step of its search. Example:

paulson@2557

218 
fast_tac (cs addss ss)

paulson@2557

219 

paulson@2557

220 
* a new logic, CHOL, the same as HOL, but with a curried syntax

paulson@2557

221 
for functions. Application looks like f a b instead of f(a,b). Also pairs

paulson@2557

222 
look like (a,b) instead of <a,b>;

paulson@2557

223 

paulson@2557

224 
* PLEASE NOTE: CHOL will eventually replace HOL!

paulson@2557

225 

paulson@2557

226 
* In CHOL, patternmatching on tuples is now available in all abstractions.

paulson@2557

227 
It translates to the operator "split". A new theory of integers is available;

paulson@2557

228 

paulson@2557

229 
* In ZF, integer numerals now denote two'scomplement binary integers.

paulson@2557

230 
Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML;

paulson@2557

231 

paulson@2557

232 
* Many new examples: I/O automata, ChurchRosser theorem, equivalents

paulson@2557

233 
of the Axiom of Choice;

paulson@2557

234 

paulson@2557

235 

paulson@2557

236 

paulson@2557

237 
New in Isabelle942

paulson@2557

238 


paulson@2557

239 

paulson@2557

240 
* Significantly faster resolution;

paulson@2557

241 

paulson@2557

242 
* the different sections in a .thy file can now be mixed and repeated

paulson@2557

243 
freely;

paulson@2557

244 

paulson@2557

245 
* Database of theorems for FOL, HOL and ZF. New

paulson@2557

246 
commands including qed, qed_goal and bind_thm store theorems in the database.

paulson@2557

247 

paulson@2557

248 
* Simple database queries: return a named theorem (get_thm) or all theorems of

paulson@2557

249 
a given theory (thms_of), or find out what theory a theorem was proved in

paulson@2557

250 
(theory_of_thm);

paulson@2557

251 

paulson@2557

252 
* Bugs fixed in the inductive definition and datatype packages;

paulson@2557

253 

paulson@2557

254 
* The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs

paulson@2557

255 
and HOL_dup_cs obsolete;

paulson@2557

256 

paulson@2557

257 
* Syntactic ambiguities caused by the new treatment of syntax in Isabelle941

paulson@2557

258 
have been removed;

paulson@2557

259 

paulson@2557

260 
* Simpler definition of function space in ZF;

paulson@2557

261 

paulson@2557

262 
* new results about cardinal and ordinal arithmetic in ZF;

paulson@2557

263 

paulson@2557

264 
* 'subtype' facility in HOL for introducing new types as subsets of existing

paulson@2557

265 
types;

paulson@2557

266 

paulson@2557

267 

wenzelm@2553

268 
$Id$
