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 

wenzelm@2971

8 
* reimplemented type inference;

wenzelm@2971

9 

wenzelm@2825

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

wenzelm@2773

11 

wenzelm@2705

12 
* added token_translation interface (may translate name tokens in

wenzelm@2756

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

wenzelm@2756

14 
the current print_mode);

wenzelm@2705

15 

wenzelm@2730

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

wenzelm@2730

17 
names in bold, underline etc. or colors;

wenzelm@2730

18 

slotosch@2653

19 
* HOLCF changes: derived all rules and arities

slotosch@2653

20 
+ axiomatic type classes instead of classes

slotosch@2653

21 
+ typedef instead of faking type definitions

paulson@2747

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

wenzelm@2730

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

slotosch@2653

24 
+ eliminated the types void, one, tr

slotosch@2653

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

slotosch@2653

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

paulson@2747

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

oheimb@2649

28 

oheimb@2639

29 
* simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.

oheimb@2639

30 

oheimb@2639

31 
* simplifier: the solver is now split into a safe and an unsafe part.

wenzelm@2732

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

wenzelm@2732

33 
functions setsolver and addsolver have been renamed to setSolver and

wenzelm@2732

34 
addSolver. added safe_asm_full_simp_tac.

oheimb@2639

35 

paulson@2747

36 
* classical reasoner: substitution with equality assumptions no longer

paulson@2747

37 
permutes other assumptions.

paulson@2747

38 

paulson@2747

39 
* classical reasoner: minor changes in semantics of addafter (now called

oheimb@2927

40 
addaltern); renamed setwrapper to setWrapper and compwrapper to compWrapper;

wenzelm@2732

41 
added safe wrapper (and access functions for it)

oheimb@2639

42 

wenzelm@2732

43 
* improved combination of classical reasoner and simplifier: new

wenzelm@2732

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

wenzelm@2732

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

paulson@2747

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

paulson@2747

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

paulson@2747

48 
old proofs, use unsafe_addss and unsafe_auto_tac

wenzelm@2553

49 

wenzelm@2556

50 
* HOL: primrec now also works with type nat;

wenzelm@2553

51 

paulson@2726

52 
* HOL: the constant for negation has been renamed from "not" to "Not" to

paulson@2726

53 
harmonize with FOL, ZF, LK, etc.

paulson@2726

54 

wenzelm@2553

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

wenzelm@2555

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

wenzelm@2553

57 

wenzelm@2553

58 
* simplifier: termless order as parameter; added interface for

wenzelm@2553

59 
simplification procedures (functions that produce *proven* rewrite

wenzelm@2553

60 
rules on the fly, depending on current redex);

wenzelm@2553

61 

wenzelm@2553

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

wenzelm@2553

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

wenzelm@2553

64 

wenzelm@2553

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

paulson@2747

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

wenzelm@2553

67 
"symbols" syntax table;

wenzelm@2553

68 

wenzelm@2553

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

wenzelm@2553

70 

wenzelm@2555

71 
* added typed_print_translation (like print_translation, but may

wenzelm@2555

72 
access type of constant);

wenzelm@2553

73 

wenzelm@2553

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

wenzelm@2553

75 
setting goals_limit);

wenzelm@2553

76 

wenzelm@2553

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

wenzelm@2553

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

wenzelm@2553

79 

paulson@2865

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

paulson@2865

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

paulson@2865

82 
as ZF_cs addSIs [equalityI];

wenzelm@2553

83 

wenzelm@2553

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

wenzelm@2553

85 

wenzelm@2553

86 
* more default rewrite rules in HOL for quantifiers, union/intersection;

wenzelm@2553

87 

wenzelm@2556

88 
* the NEWS file;

wenzelm@2553

89 

wenzelm@2554

90 

wenzelm@2732

91 

wenzelm@2553

92 
New in Isabelle947 (November 96)

wenzelm@2553

93 


wenzelm@2553

94 

wenzelm@2553

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

wenzelm@2553

96 

wenzelm@2554

97 
* superlinear speedup for large simplifications;

wenzelm@2554

98 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

103 

wenzelm@2554

104 
* improved printing of ==> : ~:

wenzelm@2554

105 

wenzelm@2554

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

wenzelm@2554

107 
and Modal (thanks to Sara Kalvala);

wenzelm@2554

108 

wenzelm@2554

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

wenzelm@2554

110 

wenzelm@2554

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

wenzelm@2554

112 
examples on HOL/Auth);

wenzelm@2554

113 

wenzelm@2554

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

wenzelm@2554

115 
the rewriter and classical reasoner simultaneously;

wenzelm@2554

116 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

119 

wenzelm@2554

120 

wenzelm@2554

121 

wenzelm@2554

122 
New in Isabelle946

wenzelm@2554

123 


wenzelm@2554

124 

wenzelm@2554

125 
* oracles  these establish an interface between Isabelle and trusted

wenzelm@2554

126 
external reasoners, which may deliver results as theorems;

wenzelm@2554

127 

wenzelm@2554

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

wenzelm@2554

129 

wenzelm@2554

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

wenzelm@2554

131 

wenzelm@2554

132 
* "constdefs" section in theory files;

wenzelm@2554

133 

wenzelm@2554

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

wenzelm@2554

135 

wenzelm@2554

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

wenzelm@2554

137 

wenzelm@2554

138 

wenzelm@2554

139 

wenzelm@2554

140 
New in Isabelle945

wenzelm@2554

141 


wenzelm@2554

142 

wenzelm@2554

143 
* reduced space requirements;

wenzelm@2554

144 

wenzelm@2554

145 
* automatic HTML generation from theories;

wenzelm@2554

146 

wenzelm@2554

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

wenzelm@2554

148 

wenzelm@2554

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

wenzelm@2554

150 

wenzelm@2554

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

wenzelm@2554

152 

wenzelm@2553

153 

paulson@2557

154 

paulson@2557

155 
New in Isabelle944

paulson@2557

156 


paulson@2557

157 

paulson@2747

158 
* greatly reduced space requirements;

paulson@2557

159 

paulson@2557

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

paulson@2557

161 

paulson@2557

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

paulson@2557

163 
page 8 of the Reference Manual);

paulson@2557

164 

paulson@2557

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

paulson@2557

166 
Axiom of Choice;

paulson@2557

167 

paulson@2557

168 
* The previous version of HOL renamed to Old_HOL;

paulson@2557

169 

paulson@2557

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

paulson@2557

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

paulson@2557

172 

paulson@2557

173 
* Mutually recursive inductive definitions finally work in HOL;

paulson@2557

174 

paulson@2557

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

paulson@2557

176 
translates to the operator "split";

paulson@2557

177 

paulson@2557

178 

paulson@2557

179 

paulson@2557

180 
New in Isabelle943

paulson@2557

181 


paulson@2557

182 

paulson@2557

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

paulson@2557

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

paulson@2557

185 
fast_tac (cs addss ss)

paulson@2557

186 

paulson@2557

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

paulson@2557

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

paulson@2557

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

paulson@2557

190 

paulson@2557

191 
* PLEASE NOTE: CHOL will eventually replace HOL!

paulson@2557

192 

paulson@2557

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

paulson@2557

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

paulson@2557

195 

paulson@2557

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

paulson@2557

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

paulson@2557

198 

paulson@2557

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

paulson@2557

200 
of the Axiom of Choice;

paulson@2557

201 

paulson@2557

202 

paulson@2557

203 

paulson@2557

204 
New in Isabelle942

paulson@2557

205 


paulson@2557

206 

paulson@2557

207 
* Significantly faster resolution;

paulson@2557

208 

paulson@2557

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

paulson@2557

210 
freely;

paulson@2557

211 

paulson@2557

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

paulson@2557

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

paulson@2557

214 

paulson@2557

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

paulson@2557

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

paulson@2557

217 
(theory_of_thm);

paulson@2557

218 

paulson@2557

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

paulson@2557

220 

paulson@2557

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

paulson@2557

222 
and HOL_dup_cs obsolete;

paulson@2557

223 

paulson@2557

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

paulson@2557

225 
have been removed;

paulson@2557

226 

paulson@2557

227 
* Simpler definition of function space in ZF;

paulson@2557

228 

paulson@2557

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

paulson@2557

230 

paulson@2557

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

paulson@2557

232 
types;

paulson@2557

233 

paulson@2557

234 

wenzelm@2553

235 
$Id$
