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

8 
* added token_translation interface (may translate name tokens in

wenzelm@2756

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

wenzelm@2756

10 
the current print_mode);

wenzelm@2705

11 

wenzelm@2730

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

wenzelm@2730

13 
names in bold, underline etc. or colors;

wenzelm@2730

14 

slotosch@2653

15 
* HOLCF changes: derived all rules and arities

slotosch@2653

16 
+ axiomatic type classes instead of classes

slotosch@2653

17 
+ typedef instead of faking type definitions

paulson@2747

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

wenzelm@2730

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

slotosch@2653

20 
+ eliminated the types void, one, tr

slotosch@2653

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

slotosch@2653

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

paulson@2747

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

oheimb@2649

24 

oheimb@2639

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

oheimb@2639

26 

oheimb@2639

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

wenzelm@2732

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

wenzelm@2732

29 
functions setsolver and addsolver have been renamed to setSolver and

wenzelm@2732

30 
addSolver. added safe_asm_full_simp_tac.

oheimb@2639

31 

paulson@2747

32 
* classical reasoner: substitution with equality assumptions no longer

paulson@2747

33 
permutes other assumptions.

paulson@2747

34 

paulson@2747

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

paulson@2747

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

wenzelm@2732

37 
added safe wrapper (and access functions for it)

oheimb@2639

38 

wenzelm@2732

39 
* improved combination of classical reasoner and simplifier: new

wenzelm@2732

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

wenzelm@2732

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

paulson@2747

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

paulson@2747

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

paulson@2747

44 
old proofs, use unsafe_addss and unsafe_auto_tac

wenzelm@2553

45 

wenzelm@2556

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

wenzelm@2553

47 

paulson@2726

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

paulson@2726

49 
harmonize with FOL, ZF, LK, etc.

paulson@2726

50 

wenzelm@2553

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

wenzelm@2555

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

wenzelm@2553

53 

wenzelm@2553

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

wenzelm@2553

55 
simplification procedures (functions that produce *proven* rewrite

wenzelm@2553

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

wenzelm@2553

57 

wenzelm@2553

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

wenzelm@2553

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

wenzelm@2553

60 

wenzelm@2553

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

paulson@2747

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

wenzelm@2553

63 
"symbols" syntax table;

wenzelm@2553

64 

wenzelm@2553

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

wenzelm@2553

66 

wenzelm@2555

67 
* added typed_print_translation (like print_translation, but may

wenzelm@2555

68 
access type of constant);

wenzelm@2553

69 

wenzelm@2553

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

wenzelm@2553

71 
setting goals_limit);

wenzelm@2553

72 

wenzelm@2553

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

wenzelm@2553

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

wenzelm@2553

75 

wenzelm@2553

76 
* ZF now has Fast_tac, Simp_tac and Auto_tac. WARNING: don't use

wenzelm@2553

77 
ZF.thy anymore! Contains fewer defs and could make a bogus simpset.

wenzelm@2553

78 
Beware of Union_iff. eq_cs is gone, can be put back as ZF_cs addSIs

wenzelm@2553

79 
[equalityI];

wenzelm@2553

80 

wenzelm@2553

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

wenzelm@2553

82 

wenzelm@2553

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

wenzelm@2553

84 

wenzelm@2556

85 
* the NEWS file;

wenzelm@2553

86 

wenzelm@2554

87 

wenzelm@2732

88 

wenzelm@2553

89 
New in Isabelle947 (November 96)

wenzelm@2553

90 


wenzelm@2553

91 

wenzelm@2553

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

wenzelm@2553

93 

wenzelm@2554

94 
* superlinear speedup for large simplifications;

wenzelm@2554

95 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

100 

wenzelm@2554

101 
* improved printing of ==> : ~:

wenzelm@2554

102 

wenzelm@2554

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

wenzelm@2554

104 
and Modal (thanks to Sara Kalvala);

wenzelm@2554

105 

wenzelm@2554

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

wenzelm@2554

107 

wenzelm@2554

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

wenzelm@2554

109 
examples on HOL/Auth);

wenzelm@2554

110 

wenzelm@2554

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

wenzelm@2554

112 
the rewriter and classical reasoner simultaneously;

wenzelm@2554

113 

wenzelm@2554

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

wenzelm@2554

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

wenzelm@2554

116 

wenzelm@2554

117 

wenzelm@2554

118 

wenzelm@2554

119 
New in Isabelle946

wenzelm@2554

120 


wenzelm@2554

121 

wenzelm@2554

122 
* oracles  these establish an interface between Isabelle and trusted

wenzelm@2554

123 
external reasoners, which may deliver results as theorems;

wenzelm@2554

124 

wenzelm@2554

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

wenzelm@2554

126 

wenzelm@2554

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

wenzelm@2554

128 

wenzelm@2554

129 
* "constdefs" section in theory files;

wenzelm@2554

130 

wenzelm@2554

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

wenzelm@2554

132 

wenzelm@2554

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

wenzelm@2554

134 

wenzelm@2554

135 

wenzelm@2554

136 

wenzelm@2554

137 
New in Isabelle945

wenzelm@2554

138 


wenzelm@2554

139 

wenzelm@2554

140 
* reduced space requirements;

wenzelm@2554

141 

wenzelm@2554

142 
* automatic HTML generation from theories;

wenzelm@2554

143 

wenzelm@2554

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

wenzelm@2554

145 

wenzelm@2554

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

wenzelm@2554

147 

wenzelm@2554

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

wenzelm@2554

149 

wenzelm@2553

150 

paulson@2557

151 

paulson@2557

152 
New in Isabelle944

paulson@2557

153 


paulson@2557

154 

paulson@2747

155 
* greatly reduced space requirements;

paulson@2557

156 

paulson@2557

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

paulson@2557

158 

paulson@2557

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

paulson@2557

160 
page 8 of the Reference Manual);

paulson@2557

161 

paulson@2557

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

paulson@2557

163 
Axiom of Choice;

paulson@2557

164 

paulson@2557

165 
* The previous version of HOL renamed to Old_HOL;

paulson@2557

166 

paulson@2557

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

paulson@2557

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

paulson@2557

169 

paulson@2557

170 
* Mutually recursive inductive definitions finally work in HOL;

paulson@2557

171 

paulson@2557

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

paulson@2557

173 
translates to the operator "split";

paulson@2557

174 

paulson@2557

175 

paulson@2557

176 

paulson@2557

177 
New in Isabelle943

paulson@2557

178 


paulson@2557

179 

paulson@2557

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

paulson@2557

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

paulson@2557

182 
fast_tac (cs addss ss)

paulson@2557

183 

paulson@2557

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

paulson@2557

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

paulson@2557

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

paulson@2557

187 

paulson@2557

188 
* PLEASE NOTE: CHOL will eventually replace HOL!

paulson@2557

189 

paulson@2557

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

paulson@2557

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

paulson@2557

192 

paulson@2557

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

paulson@2557

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

paulson@2557

195 

paulson@2557

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

paulson@2557

197 
of the Axiom of Choice;

paulson@2557

198 

paulson@2557

199 

paulson@2557

200 

paulson@2557

201 
New in Isabelle942

paulson@2557

202 


paulson@2557

203 

paulson@2557

204 
* Significantly faster resolution;

paulson@2557

205 

paulson@2557

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

paulson@2557

207 
freely;

paulson@2557

208 

paulson@2557

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

paulson@2557

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

paulson@2557

211 

paulson@2557

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

paulson@2557

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

paulson@2557

214 
(theory_of_thm);

paulson@2557

215 

paulson@2557

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

paulson@2557

217 

paulson@2557

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

paulson@2557

219 
and HOL_dup_cs obsolete;

paulson@2557

220 

paulson@2557

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

paulson@2557

222 
have been removed;

paulson@2557

223 

paulson@2557

224 
* Simpler definition of function space in ZF;

paulson@2557

225 

paulson@2557

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

paulson@2557

227 

paulson@2557

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

paulson@2557

229 
types;

paulson@2557

230 

paulson@2557

231 

wenzelm@2553

232 
$Id$
