wenzelm@2553

1 

wenzelm@2553

2 
Isabelle NEWS  history of uservisible changes

wenzelm@2553

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

wenzelm@2553

4 

wenzelm@2730

5 
New in Isabelle948 (April 1997)

wenzelm@2731

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 

paulson@3002

15 
* reimplemented type inference for greater efficiency;

paulson@3002

16 

paulson@3002

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

paulson@3002

18 
setting goals_limit);

paulson@3002

19 

paulson@3002

20 
*** Syntax

paulson@3002

21 

paulson@3002

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

paulson@3002

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

paulson@3002

24 
"symbols" syntax table;

paulson@3002

25 

wenzelm@2705

26 
* added token_translation interface (may translate name tokens in

wenzelm@2756

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

wenzelm@2756

28 
the current print_mode);

wenzelm@2705

29 

wenzelm@2730

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

wenzelm@2730

31 
names in bold, underline etc. or colors;

wenzelm@2730

32 

paulson@3002

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

paulson@3002

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

paulson@3002

35 

paulson@3002

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

paulson@3002

37 

paulson@3002

38 
* added typed_print_translation (like print_translation, but may

paulson@3002

39 
access type of constant);

paulson@3002

40 

paulson@3002

41 
*** Classical Reasoner ***

paulson@3002

42 

paulson@3002

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

paulson@3002

44 
some limitations. Blast_tac...

paulson@3002

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

paulson@3002

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

paulson@3002

47 
(the conclusion MUST be a formula variable)

paulson@3002

48 
+ ignores types, which can make HOL proofs fail

paulson@3002

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

paulson@3002

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

paulson@3002

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

paulson@3002

52 

paulson@3002

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

paulson@3002

54 

paulson@3002

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

paulson@3002

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

paulson@3002

57 
(and access functions for it)

paulson@3002

58 

paulson@3002

59 
* improved combination of classical reasoner and simplifier: new

paulson@3002

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

paulson@3002

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

paulson@3002

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

paulson@3002

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

paulson@3002

64 
old proofs, use unsafe_addss and unsafe_auto_tac

paulson@3002

65 

paulson@3002

66 
*** Simplifier ***

paulson@3002

67 

paulson@3002

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

paulson@3002

69 

paulson@3002

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

paulson@3002

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

paulson@3002

72 
functions setsolver and addsolver have been renamed to setSolver and

paulson@3002

73 
addSolver. added safe_asm_full_simp_tac.

paulson@3002

74 

paulson@3002

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

paulson@3002

76 
added interface for simplification procedures (functions that produce *proven*

paulson@3002

77 
rewrite rules on the fly, depending on current redex);

paulson@3002

78 

paulson@3002

79 
*** HOL ***

paulson@3002

80 

paulson@3002

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

paulson@3002

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

paulson@3002

83 

paulson@3002

84 
* primrec now also works with type nat;

paulson@3002

85 

paulson@3002

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

paulson@3002

87 
harmonize with FOL, ZF, LK, etc.

paulson@3002

88 

paulson@3002

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

paulson@3002

90 

paulson@3002

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

paulson@3002

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

paulson@3002

93 

paulson@3002

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

paulson@3002

95 

paulson@3002

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

paulson@3002

97 

slotosch@2653

98 
* HOLCF changes: derived all rules and arities

slotosch@2653

99 
+ axiomatic type classes instead of classes

slotosch@2653

100 
+ typedef instead of faking type definitions

paulson@2747

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

wenzelm@2730

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

slotosch@2653

103 
+ eliminated the types void, one, tr

slotosch@2653

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

slotosch@2653

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

paulson@2747

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

oheimb@2649

107 

paulson@3002

108 
*** ZF ***

wenzelm@2553

109 

paulson@2865

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

paulson@2865

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

paulson@2865

112 
as ZF_cs addSIs [equalityI];

wenzelm@2553

113 

wenzelm@2554

114 

wenzelm@2732

115 

wenzelm@2553

116 
New in Isabelle947 (November 96)

wenzelm@2553

117 


wenzelm@2553

118 

wenzelm@2553

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

wenzelm@2553

120 

wenzelm@2554

121 
* superlinear speedup for large simplifications;

wenzelm@2554

122 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

127 

wenzelm@2554

128 
* improved printing of ==> : ~:

wenzelm@2554

129 

wenzelm@2554

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

wenzelm@2554

131 
and Modal (thanks to Sara Kalvala);

wenzelm@2554

132 

wenzelm@2554

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

wenzelm@2554

134 

wenzelm@2554

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

wenzelm@2554

136 
examples on HOL/Auth);

wenzelm@2554

137 

wenzelm@2554

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

wenzelm@2554

139 
the rewriter and classical reasoner simultaneously;

wenzelm@2554

140 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

143 

wenzelm@2554

144 

wenzelm@2554

145 

wenzelm@2554

146 
New in Isabelle946

wenzelm@2554

147 


wenzelm@2554

148 

wenzelm@2554

149 
* oracles  these establish an interface between Isabelle and trusted

wenzelm@2554

150 
external reasoners, which may deliver results as theorems;

wenzelm@2554

151 

wenzelm@2554

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

wenzelm@2554

153 

wenzelm@2554

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

wenzelm@2554

155 

wenzelm@2554

156 
* "constdefs" section in theory files;

wenzelm@2554

157 

wenzelm@2554

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

wenzelm@2554

159 

wenzelm@2554

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

wenzelm@2554

161 

wenzelm@2554

162 

wenzelm@2554

163 

wenzelm@2554

164 
New in Isabelle945

wenzelm@2554

165 


wenzelm@2554

166 

wenzelm@2554

167 
* reduced space requirements;

wenzelm@2554

168 

wenzelm@2554

169 
* automatic HTML generation from theories;

wenzelm@2554

170 

wenzelm@2554

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

wenzelm@2554

172 

wenzelm@2554

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

wenzelm@2554

174 

wenzelm@2554

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

wenzelm@2554

176 

wenzelm@2553

177 

paulson@2557

178 

paulson@2557

179 
New in Isabelle944

paulson@2557

180 


paulson@2557

181 

paulson@2747

182 
* greatly reduced space requirements;

paulson@2557

183 

paulson@2557

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

paulson@2557

185 

paulson@2557

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

paulson@2557

187 
page 8 of the Reference Manual);

paulson@2557

188 

paulson@2557

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

paulson@2557

190 
Axiom of Choice;

paulson@2557

191 

paulson@2557

192 
* The previous version of HOL renamed to Old_HOL;

paulson@2557

193 

paulson@2557

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

paulson@2557

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

paulson@2557

196 

paulson@2557

197 
* Mutually recursive inductive definitions finally work in HOL;

paulson@2557

198 

paulson@2557

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

paulson@2557

200 
translates to the operator "split";

paulson@2557

201 

paulson@2557

202 

paulson@2557

203 

paulson@2557

204 
New in Isabelle943

paulson@2557

205 


paulson@2557

206 

paulson@2557

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

paulson@2557

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

paulson@2557

209 
fast_tac (cs addss ss)

paulson@2557

210 

paulson@2557

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

paulson@2557

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

paulson@2557

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

paulson@2557

214 

paulson@2557

215 
* PLEASE NOTE: CHOL will eventually replace HOL!

paulson@2557

216 

paulson@2557

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

paulson@2557

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

paulson@2557

219 

paulson@2557

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

paulson@2557

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

paulson@2557

222 

paulson@2557

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

paulson@2557

224 
of the Axiom of Choice;

paulson@2557

225 

paulson@2557

226 

paulson@2557

227 

paulson@2557

228 
New in Isabelle942

paulson@2557

229 


paulson@2557

230 

paulson@2557

231 
* Significantly faster resolution;

paulson@2557

232 

paulson@2557

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

paulson@2557

234 
freely;

paulson@2557

235 

paulson@2557

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

paulson@2557

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

paulson@2557

238 

paulson@2557

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

paulson@2557

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

paulson@2557

241 
(theory_of_thm);

paulson@2557

242 

paulson@2557

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

paulson@2557

244 

paulson@2557

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

paulson@2557

246 
and HOL_dup_cs obsolete;

paulson@2557

247 

paulson@2557

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

paulson@2557

249 
have been removed;

paulson@2557

250 

paulson@2557

251 
* Simpler definition of function space in ZF;

paulson@2557

252 

paulson@2557

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

paulson@2557

254 

paulson@2557

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

paulson@2557

256 
types;

paulson@2557

257 

paulson@2557

258 

wenzelm@2553

259 
$Id$
