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 * supports alternative (named) syntax tables (parser and pretty
25 printer); internal interface is provided by add_modesyntax(_i);
27 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
28 be used in conjunction with the Isabelle symbol font; uses the
29 "symbols" syntax table;
31 * added token_translation interface (may translate name tokens in
32 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
33 the current print_mode); IMPORTANT: user print translation functions
34 are responsible for marking newly introduced bounds
37 * token translations for modes "xterm" and "xterm_color" that display
38 names in bold, underline etc. or colors (which requires a color
41 * infixes may now be declared with names independent of their syntax;
43 * added typed_print_translation (like print_translation, but may
44 access type of constant);
47 *** Classical Reasoner ***
49 Blast_tac: a new tactic! It is often more powerful than fast_tac, but has
50 some limitations. Blast_tac...
51 + ignores addss, addbefore, addafter; this restriction is intrinsic
52 + ignores elimination rules that don't have the correct format
53 (the conclusion MUST be a formula variable)
54 + ignores types, which can make HOL proofs fail
55 + rules must not require higher-order unification, e.g. apply_type in ZF
56 [message "Function Var's argument not a bound variable" relates to this]
57 + its proof strategy is more general but can actually be slower
59 * substitution with equality assumptions no longer permutes other
62 * minor changes in semantics of addafter (now called addaltern); renamed
63 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
64 (and access functions for it);
66 * improved combination of classical reasoner and simplifier: new
67 addss, auto_tac, functions for handling clasimpsets, ... Now, the
68 simplification is safe (therefore moved to safe_step_tac) and thus
69 more complete, as multiple instantiation of unknowns (with slow_tac).
70 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
71 old proofs, use unsafe_addss and unsafe_auto_tac;
76 * added interface for simplification procedures (functions that
77 produce *proven* rewrite rules on the fly, depending on current
80 * ordering on terms as parameter (used for ordered rewriting);
82 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
84 * the solver is now split into a safe and an unsafe part.
85 This should be invisible for the normal user, except that the
86 functions setsolver and addsolver have been renamed to setSolver and
87 addSolver; added safe_asm_full_simp_tac;
92 * a generic induction tactic `induct_tac' which works for all datatypes and
95 * patterns in case expressions allow tuple patterns as arguments to
96 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
98 * primrec now also works with type nat;
100 * the constant for negation has been renamed from "not" to "Not" to
101 harmonize with FOL, ZF, LK, etc.;
103 * HOL/ex/LFilter theory of a corecursive "filter" functional for
106 * HOL/ex/Ring.thy declares cring_simp, which solves equational
107 problems in commutative rings, using axiomatic type classes for + and *;
109 * more examples in HOL/MiniML and HOL/Auth;
111 * more default rewrite rules for quantifiers, union/intersection;
113 * HOLCF/IOA replaces old HOL/IOA;
115 * HOLCF changes: derived all rules and arities
116 + axiomatic type classes instead of classes
117 + typedef instead of faking type definitions
118 + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
119 + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
120 + eliminated the types void, one, tr
121 + use unit lift and bool lift (with translations) instead of one and tr
122 + eliminated blift from Lift3.thy (use Def instead of blift)
123 all eliminated rules are derived as theorems --> no visible changes ;
128 * ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default
129 rewrite rule; this may affect some proofs. eq_cs is gone but can be put back
130 as ZF_cs addSIs [equalityI];
134 New in Isabelle94-7 (November 96)
135 ---------------------------------
137 * allowing negative levels (as offsets) in prlev and choplev;
139 * super-linear speedup for large simplifications;
141 * FOL, ZF and HOL now use miniscoping: rewriting pushes
142 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
143 FAIL); can suppress it using the command Delsimps (ex_simps @
144 all_simps); De Morgan laws are also now included, by default;
146 * improved printing of ==> : ~:
148 * new object-logic "Sequents" adds linear logic, while replacing LK
149 and Modal (thanks to Sara Kalvala);
151 * HOL/Auth: correctness proofs for authentication protocols;
153 * HOL: new auto_tac combines rewriting and classical reasoning (many
154 examples on HOL/Auth);
156 * HOL: new command AddIffs for declaring theorems of the form P=Q to
157 the rewriter and classical reasoner simultaneously;
159 * function uresult no longer returns theorems in "standard" format;
160 regain previous version by: val uresult = standard o uresult;
167 * oracles -- these establish an interface between Isabelle and trusted
168 external reasoners, which may deliver results as theorems;
170 * proof objects (in particular record all uses of oracles);
172 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
174 * "constdefs" section in theory files;
176 * "primrec" section (HOL) no longer requires names;
178 * internal type "tactic" now simply "thm -> thm Sequence.seq";
185 * reduced space requirements;
187 * automatic HTML generation from theories;
189 * theory files no longer require "..." (quotes) around most types;
191 * new examples, including two proofs of the Church-Rosser theorem;
193 * non-curried (1994) version of HOL is no longer distributed;
200 * greatly reduced space requirements;
202 * theory files (.thy) no longer require \...\ escapes at line breaks;
204 * searchable theorem database (see the section "Retrieving theorems" on
205 page 8 of the Reference Manual);
207 * new examples, including Grabczewski's monumental case study of the
210 * The previous version of HOL renamed to Old_HOL;
212 * The new version of HOL (previously called CHOL) uses a curried syntax
213 for functions. Application looks like f a b instead of f(a,b);
215 * Mutually recursive inductive definitions finally work in HOL;
217 * In ZF, pattern-matching on tuples is now available in all abstractions and
218 translates to the operator "split";
225 * new infix operator, addss, allowing the classical reasoner to
226 perform simplification at each step of its search. Example:
227 fast_tac (cs addss ss)
229 * a new logic, CHOL, the same as HOL, but with a curried syntax
230 for functions. Application looks like f a b instead of f(a,b). Also pairs
231 look like (a,b) instead of <a,b>;
233 * PLEASE NOTE: CHOL will eventually replace HOL!
235 * In CHOL, pattern-matching on tuples is now available in all abstractions.
236 It translates to the operator "split". A new theory of integers is available;
238 * In ZF, integer numerals now denote two's-complement binary integers.
239 Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML;
241 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
242 of the Axiom of Choice;
249 * Significantly faster resolution;
251 * the different sections in a .thy file can now be mixed and repeated
254 * Database of theorems for FOL, HOL and ZF. New
255 commands including qed, qed_goal and bind_thm store theorems in the database.
257 * Simple database queries: return a named theorem (get_thm) or all theorems of
258 a given theory (thms_of), or find out what theory a theorem was proved in
261 * Bugs fixed in the inductive definition and datatype packages;
263 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
264 and HOL_dup_cs obsolete;
266 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
269 * Simpler definition of function space in ZF;
271 * new results about cardinal and ordinal arithmetic in ZF;
273 * 'subtype' facility in HOL for introducing new types as subsets of existing