2 Isabelle NEWS -- history of user-visible changes
3 ================================================
5 New in Isabelle94-8 (May 1997)
6 ------------------------------
8 *** General Changes ***
10 * new utilities to build / run / maintain Isabelle etc. (in parts
11 still somewhat experimental); old Makefiles etc. still functional;
13 * INSTALL text, together with ./configure and ./build scripts;
15 * reimplemented type inference for greater efficiency, better error
16 messages and clean internal interface;
18 * prlim command for dealing with lots of subgoals (an easier way of
24 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
25 be used in conjunction with the Isabelle symbol font; uses the
26 "symbols" syntax table;
28 * added token_translation interface (may translate name tokens in
29 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
30 the current print_mode);
32 * token translations for modes "xterm" and "xterm_color" that display
33 names in bold, underline etc. or colors (which requires a color
36 * now supports alternative (named) syntax tables (parser and pretty
37 printer); internal interface is provided by add_modesyntax(_i);
39 * infixes may now be declared with names independent of their syntax;
41 * added typed_print_translation (like print_translation, but may
42 access type of constant);
45 *** Classical Reasoner ***
47 Blast_tac: a new tactic! It is often more powerful than fast_tac, but has
48 some limitations. Blast_tac...
49 + ignores addss, addbefore, addafter; this restriction is intrinsic
50 + ignores elimination rules that don't have the correct format
51 (the conclusion MUST be a formula variable)
52 + ignores types, which can make HOL proofs fail
53 + rules must not require higher-order unification, e.g. apply_type in ZF
54 [message "Function Var's argument not a bound variable" relates to this]
55 + its proof strategy is more general but can actually be slower
57 * substitution with equality assumptions no longer permutes other assumptions.
59 * minor changes in semantics of addafter (now called addaltern); renamed
60 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
61 (and access functions for it)
63 * improved combination of classical reasoner and simplifier: new
64 addss, auto_tac, functions for handling clasimpsets, ... Now, the
65 simplification is safe (therefore moved to safe_step_tac) and thus
66 more complete, as multiple instantiation of unknowns (with slow_tac).
67 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
68 old proofs, use unsafe_addss and unsafe_auto_tac
73 * added interface for simplification procedures (functions that
74 produce *proven* rewrite rules on the fly, depending on current
77 * ordering on terms as parameter (used for ordered rewriting);
79 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
81 * the solver is now split into a safe and an unsafe part.
82 This should be invisible for the normal user, except that the
83 functions setsolver and addsolver have been renamed to setSolver and
84 addSolver. added safe_asm_full_simp_tac.
89 * a generic induction tactic `induct_tac' which works for all datatypes and
92 * patterns in case expressions allow tuple patterns as arguments to
93 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
95 * primrec now also works with type nat;
97 * the constant for negation has been renamed from "not" to "Not" to
98 harmonize with FOL, ZF, LK, etc.
100 * HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists
102 * HOL/ex/Ring.thy declares cring_simp, which solves equational
103 problems in commutative rings, using axiomatic type classes for + and *;
105 * more examples in HOL/MiniML and HOL/Auth;
107 * more default rewrite rules for quantifiers, union/intersection;
109 * HOLCF changes: derived all rules and arities
110 + axiomatic type classes instead of classes
111 + typedef instead of faking type definitions
112 + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
113 + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
114 + eliminated the types void, one, tr
115 + use unit lift and bool lift (with translations) instead of one and tr
116 + eliminated blift from Lift3.thy (use Def instead of blift)
117 all eliminated rules are derived as theorems --> no visible changes
122 * ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default
123 rewrite rule; this may affect some proofs. eq_cs is gone but can be put back
124 as ZF_cs addSIs [equalityI];
128 New in Isabelle94-7 (November 96)
129 ---------------------------------
131 * allowing negative levels (as offsets) in prlev and choplev;
133 * super-linear speedup for large simplifications;
135 * FOL, ZF and HOL now use miniscoping: rewriting pushes
136 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
137 FAIL); can suppress it using the command Delsimps (ex_simps @
138 all_simps); De Morgan laws are also now included, by default;
140 * improved printing of ==> : ~:
142 * new object-logic "Sequents" adds linear logic, while replacing LK
143 and Modal (thanks to Sara Kalvala);
145 * HOL/Auth: correctness proofs for authentication protocols;
147 * HOL: new auto_tac combines rewriting and classical reasoning (many
148 examples on HOL/Auth);
150 * HOL: new command AddIffs for declaring theorems of the form P=Q to
151 the rewriter and classical reasoner simultaneously;
153 * function uresult no longer returns theorems in "standard" format;
154 regain previous version by: val uresult = standard o uresult;
161 * oracles -- these establish an interface between Isabelle and trusted
162 external reasoners, which may deliver results as theorems;
164 * proof objects (in particular record all uses of oracles);
166 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
168 * "constdefs" section in theory files;
170 * "primrec" section (HOL) no longer requires names;
172 * internal type "tactic" now simply "thm -> thm Sequence.seq";
179 * reduced space requirements;
181 * automatic HTML generation from theories;
183 * theory files no longer require "..." (quotes) around most types;
185 * new examples, including two proofs of the Church-Rosser theorem;
187 * non-curried (1994) version of HOL is no longer distributed;
194 * greatly reduced space requirements;
196 * theory files (.thy) no longer require \...\ escapes at line breaks;
198 * searchable theorem database (see the section "Retrieving theorems" on
199 page 8 of the Reference Manual);
201 * new examples, including Grabczewski's monumental case study of the
204 * The previous version of HOL renamed to Old_HOL;
206 * The new version of HOL (previously called CHOL) uses a curried syntax
207 for functions. Application looks like f a b instead of f(a,b);
209 * Mutually recursive inductive definitions finally work in HOL;
211 * In ZF, pattern-matching on tuples is now available in all abstractions and
212 translates to the operator "split";
219 * new infix operator, addss, allowing the classical reasoner to
220 perform simplification at each step of its search. Example:
221 fast_tac (cs addss ss)
223 * a new logic, CHOL, the same as HOL, but with a curried syntax
224 for functions. Application looks like f a b instead of f(a,b). Also pairs
225 look like (a,b) instead of <a,b>;
227 * PLEASE NOTE: CHOL will eventually replace HOL!
229 * In CHOL, pattern-matching on tuples is now available in all abstractions.
230 It translates to the operator "split". A new theory of integers is available;
232 * In ZF, integer numerals now denote two's-complement binary integers.
233 Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML;
235 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
236 of the Axiom of Choice;
243 * Significantly faster resolution;
245 * the different sections in a .thy file can now be mixed and repeated
248 * Database of theorems for FOL, HOL and ZF. New
249 commands including qed, qed_goal and bind_thm store theorems in the database.
251 * Simple database queries: return a named theorem (get_thm) or all theorems of
252 a given theory (thms_of), or find out what theory a theorem was proved in
255 * Bugs fixed in the inductive definition and datatype packages;
257 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
258 and HOL_dup_cs obsolete;
260 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
263 * Simpler definition of function space in ZF;
265 * new results about cardinal and ordinal arithmetic in ZF;
267 * 'subtype' facility in HOL for introducing new types as subsets of existing