summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

author | wenzelm |

Fri Mar 07 13:21:15 1997 +0100 (1997-03-07) | |

changeset 2756 | 643cba384a61 |

parent 2747 | 9fdc1461085f |

child 2773 | 36fdd908a26c |

permissions | -rw-r--r-- |

*** empty log message ***

2 Isabelle NEWS -- history of user-visible changes

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

5 New in Isabelle94-8 (April 1997)

6 --------------------------------

8 * added token_translation interface (may translate name tokens in

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

10 the current print_mode);

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

13 names in bold, underline etc. or colors;

15 * HOLCF changes: derived all rules and arities

16 + axiomatic type classes instead of classes

17 + typedef instead of faking type definitions

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

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

20 + eliminated the types void, one, tr

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

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

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

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

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

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

29 functions setsolver and addsolver have been renamed to setSolver and

30 addSolver. added safe_asm_full_simp_tac.

32 * classical reasoner: substitution with equality assumptions no longer

33 permutes other assumptions.

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

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

37 added safe wrapper (and access functions for it)

39 * improved combination of classical reasoner and simplifier: new

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

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

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

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

44 old proofs, use unsafe_addss and unsafe_auto_tac

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

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

49 harmonize with FOL, ZF, LK, etc.

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

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

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

55 simplification procedures (functions that produce *proven* rewrite

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

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

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

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

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

63 "symbols" syntax table;

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

67 * added typed_print_translation (like print_translation, but may

68 access type of constant);

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

71 setting goals_limit);

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

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

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

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

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

79 [equalityI];

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

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

85 * the NEWS file;

89 New in Isabelle94-7 (November 96)

90 ---------------------------------

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

94 * super-linear speedup for large simplifications;

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

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

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

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

101 * improved printing of ==> : ~:

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

104 and Modal (thanks to Sara Kalvala);

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

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

109 examples on HOL/Auth);

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

112 the rewriter and classical reasoner simultaneously;

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

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

119 New in Isabelle94-6

120 -------------------

122 * oracles -- these establish an interface between Isabelle and trusted

123 external reasoners, which may deliver results as theorems;

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

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

129 * "constdefs" section in theory files;

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

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

137 New in Isabelle94-5

138 -------------------

140 * reduced space requirements;

142 * automatic HTML generation from theories;

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

146 * new examples, including two proofs of the Church-Rosser theorem;

148 * non-curried (1994) version of HOL is no longer distributed;

152 New in Isabelle94-4

153 -------------------

155 * greatly reduced space requirements;

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

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

160 page 8 of the Reference Manual);

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

163 Axiom of Choice;

165 * The previous version of HOL renamed to Old_HOL;

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

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

170 * Mutually recursive inductive definitions finally work in HOL;

172 * In ZF, pattern-matching on tuples is now available in all abstractions and

173 translates to the operator "split";

177 New in Isabelle94-3

178 -------------------

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

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

182 fast_tac (cs addss ss)

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

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

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

188 * PLEASE NOTE: CHOL will eventually replace HOL!

190 * In CHOL, pattern-matching on tuples is now available in all abstractions.

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

193 * In ZF, integer numerals now denote two's-complement binary integers.

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

196 * Many new examples: I/O automata, Church-Rosser theorem, equivalents

197 of the Axiom of Choice;

201 New in Isabelle94-2

202 -------------------

204 * Significantly faster resolution;

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

207 freely;

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

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

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

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

214 (theory_of_thm);

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

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

219 and HOL_dup_cs obsolete;

221 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1

222 have been removed;

224 * Simpler definition of function space in ZF;

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

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

229 types;

232 $Id$