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@2825

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

wenzelm@2773

9 

wenzelm@2705

10 
* added token_translation interface (may translate name tokens in

wenzelm@2756

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

wenzelm@2756

12 
the current print_mode);

wenzelm@2705

13 

wenzelm@2730

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

wenzelm@2730

15 
names in bold, underline etc. or colors;

wenzelm@2730

16 

slotosch@2653

17 
* HOLCF changes: derived all rules and arities

slotosch@2653

18 
+ axiomatic type classes instead of classes

slotosch@2653

19 
+ typedef instead of faking type definitions

paulson@2747

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

wenzelm@2730

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

slotosch@2653

22 
+ eliminated the types void, one, tr

slotosch@2653

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

slotosch@2653

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

paulson@2747

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

oheimb@2649

26 

oheimb@2639

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

oheimb@2639

28 

oheimb@2639

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

wenzelm@2732

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

wenzelm@2732

31 
functions setsolver and addsolver have been renamed to setSolver and

wenzelm@2732

32 
addSolver. added safe_asm_full_simp_tac.

oheimb@2639

33 

paulson@2747

34 
* classical reasoner: substitution with equality assumptions no longer

paulson@2747

35 
permutes other assumptions.

paulson@2747

36 

paulson@2747

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

paulson@2747

38 
addaltern); renamed setwrapper to setWrapper and addwrapper to addWrapper;

wenzelm@2732

39 
added safe wrapper (and access functions for it)

oheimb@2639

40 

wenzelm@2732

41 
* improved combination of classical reasoner and simplifier: new

wenzelm@2732

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

wenzelm@2732

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

paulson@2747

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

paulson@2747

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

paulson@2747

46 
old proofs, use unsafe_addss and unsafe_auto_tac

wenzelm@2553

47 

wenzelm@2556

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

wenzelm@2553

49 

paulson@2726

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

paulson@2726

51 
harmonize with FOL, ZF, LK, etc.

paulson@2726

52 

wenzelm@2553

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

wenzelm@2555

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

wenzelm@2553

55 

wenzelm@2553

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

wenzelm@2553

57 
simplification procedures (functions that produce *proven* rewrite

wenzelm@2553

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

wenzelm@2553

59 

wenzelm@2553

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

wenzelm@2553

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

wenzelm@2553

62 

wenzelm@2553

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

paulson@2747

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

wenzelm@2553

65 
"symbols" syntax table;

wenzelm@2553

66 

wenzelm@2553

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

wenzelm@2553

68 

wenzelm@2555

69 
* added typed_print_translation (like print_translation, but may

wenzelm@2555

70 
access type of constant);

wenzelm@2553

71 

wenzelm@2553

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

wenzelm@2553

73 
setting goals_limit);

wenzelm@2553

74 

wenzelm@2553

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

wenzelm@2553

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

wenzelm@2553

77 

paulson@2865

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

paulson@2865

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

paulson@2865

80 
as ZF_cs addSIs [equalityI];

wenzelm@2553

81 

wenzelm@2553

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

wenzelm@2553

83 

wenzelm@2553

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

wenzelm@2553

85 

wenzelm@2556

86 
* the NEWS file;

wenzelm@2553

87 

wenzelm@2554

88 

wenzelm@2732

89 

wenzelm@2553

90 
New in Isabelle947 (November 96)

wenzelm@2553

91 


wenzelm@2553

92 

wenzelm@2553

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

wenzelm@2553

94 

wenzelm@2554

95 
* superlinear speedup for large simplifications;

wenzelm@2554

96 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

101 

wenzelm@2554

102 
* improved printing of ==> : ~:

wenzelm@2554

103 

wenzelm@2554

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

wenzelm@2554

105 
and Modal (thanks to Sara Kalvala);

wenzelm@2554

106 

wenzelm@2554

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

wenzelm@2554

108 

wenzelm@2554

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

wenzelm@2554

110 
examples on HOL/Auth);

wenzelm@2554

111 

wenzelm@2554

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

wenzelm@2554

113 
the rewriter and classical reasoner simultaneously;

wenzelm@2554

114 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

117 

wenzelm@2554

118 

wenzelm@2554

119 

wenzelm@2554

120 
New in Isabelle946

wenzelm@2554

121 


wenzelm@2554

122 

wenzelm@2554

123 
* oracles  these establish an interface between Isabelle and trusted

wenzelm@2554

124 
external reasoners, which may deliver results as theorems;

wenzelm@2554

125 

wenzelm@2554

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

wenzelm@2554

127 

wenzelm@2554

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

wenzelm@2554

129 

wenzelm@2554

130 
* "constdefs" section in theory files;

wenzelm@2554

131 

wenzelm@2554

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

wenzelm@2554

133 

wenzelm@2554

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

wenzelm@2554

135 

wenzelm@2554

136 

wenzelm@2554

137 

wenzelm@2554

138 
New in Isabelle945

wenzelm@2554

139 


wenzelm@2554

140 

wenzelm@2554

141 
* reduced space requirements;

wenzelm@2554

142 

wenzelm@2554

143 
* automatic HTML generation from theories;

wenzelm@2554

144 

wenzelm@2554

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

wenzelm@2554

146 

wenzelm@2554

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

wenzelm@2554

148 

wenzelm@2554

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

wenzelm@2554

150 

wenzelm@2553

151 

paulson@2557

152 

paulson@2557

153 
New in Isabelle944

paulson@2557

154 


paulson@2557

155 

paulson@2747

156 
* greatly reduced space requirements;

paulson@2557

157 

paulson@2557

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

paulson@2557

159 

paulson@2557

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

paulson@2557

161 
page 8 of the Reference Manual);

paulson@2557

162 

paulson@2557

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

paulson@2557

164 
Axiom of Choice;

paulson@2557

165 

paulson@2557

166 
* The previous version of HOL renamed to Old_HOL;

paulson@2557

167 

paulson@2557

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

paulson@2557

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

paulson@2557

170 

paulson@2557

171 
* Mutually recursive inductive definitions finally work in HOL;

paulson@2557

172 

paulson@2557

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

paulson@2557

174 
translates to the operator "split";

paulson@2557

175 

paulson@2557

176 

paulson@2557

177 

paulson@2557

178 
New in Isabelle943

paulson@2557

179 


paulson@2557

180 

paulson@2557

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

paulson@2557

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

paulson@2557

183 
fast_tac (cs addss ss)

paulson@2557

184 

paulson@2557

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

paulson@2557

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

paulson@2557

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

paulson@2557

188 

paulson@2557

189 
* PLEASE NOTE: CHOL will eventually replace HOL!

paulson@2557

190 

paulson@2557

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

paulson@2557

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

paulson@2557

193 

paulson@2557

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

paulson@2557

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

paulson@2557

196 

paulson@2557

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

paulson@2557

198 
of the Axiom of Choice;

paulson@2557

199 

paulson@2557

200 

paulson@2557

201 

paulson@2557

202 
New in Isabelle942

paulson@2557

203 


paulson@2557

204 

paulson@2557

205 
* Significantly faster resolution;

paulson@2557

206 

paulson@2557

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

paulson@2557

208 
freely;

paulson@2557

209 

paulson@2557

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

paulson@2557

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

paulson@2557

212 

paulson@2557

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

paulson@2557

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

paulson@2557

215 
(theory_of_thm);

paulson@2557

216 

paulson@2557

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

paulson@2557

218 

paulson@2557

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

paulson@2557

220 
and HOL_dup_cs obsolete;

paulson@2557

221 

paulson@2557

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

paulson@2557

223 
have been removed;

paulson@2557

224 

paulson@2557

225 
* Simpler definition of function space in ZF;

paulson@2557

226 

paulson@2557

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

paulson@2557

228 

paulson@2557

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

paulson@2557

230 
types;

paulson@2557

231 

paulson@2557

232 

wenzelm@2553

233 
$Id$
