--- a/NEWS Fri Sep 15 20:47:06 2000 +0200
+++ b/NEWS Fri Sep 15 21:49:54 2000 +0200
@@ -2,10 +2,10 @@
Isabelle NEWS -- history user-relevant changes
==============================================
-New in this Isabelle version
-----------------------------
+New in Isabelle99-1 (September 2000)
+------------------------------------
-*** Overview of INCOMPATIBILITIES (see below for more details) ***
+*** Overview of INCOMPATIBILITIES ***
* HOL: simplification of natural numbers is much changed; to partly
recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)
@@ -14,40 +14,43 @@
Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
-* HOL: 0 is now overloaded, so the type constraint ::nat may sometimes be
-needed;
+* HOL: simplification no longer dives into case-expressions;
+
+* HOL: nat_less_induct renamed to less_induct;
+
+* HOL: systematic renaming of the SOME (Eps) rules, may use isatool
+fixsome to patch .thy and .ML sources automatically;
-* HOL: the constant for f``x is now "image" rather than "op ``";
+ select_equality -> some_equality
+ select_eq_Ex -> some_eq_ex
+ selectI2EX -> someI2_ex
+ selectI2 -> someI2
+ selectI -> someI
+ select1_equality -> some1_equality
+ Eps_sym_eq -> some_sym_eq_trivial
+ Eps_eq -> some_eq_trivial
+
+* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
+
+* HOL: removed obsolete theorem binding expand_if (refer to split_if
+instead);
+
+* HOL: the recursion equations generated by 'recdef' are now called
+f.simps instead of f.rules;
+
+* HOL: qed_spec_mp now also handles bounded ALL as well;
+
+* HOL: 0 is now overloaded, so the type constraint ":: nat" may
+sometimes be needed;
+
+* HOL: the constant for "f``x" is now "image" rather than "op ``";
* HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian
product is now "<*>" instead of "Times"; the lexicographic product is
now "<*lex*>" instead of "**";
-* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
-
-* HOL: simplification no longer dives into case-expressions;
-
-* HOL: the recursion equations generated by 'recdef' are now called
-f.simps instead of f.rules;
-
-* HOL: theory Sexp now in HOL/Induct examples (it used to be part of
-main HOL, but was unused); it is better to use HOL's datatype package
-anyway;
-
-* HOL: removed obsolete theorem binding expand_if (refer to split_if
-instead);
-
-* HOL: less_induct is renamed nat_less_induct
-
-* HOL: systematic renaming of the @-rules:
- selectI -> someI
- selectI2 -> someI2
- selectI2EX -> someI2_ex
- select_equality -> some_equality
- select1_equality -> some1_equality
- select_eq_Ex -> some_eq_ex
- Eps_eq -> some_eq_trivial
- Eps_sym_eq -> some_sym_eq_trivial
+* HOL: theory Sexp is now in HOL/Induct examples (it used to be part
+of main HOL, but was unused); better use HOL's datatype package;
* HOL/Real: "rabs" replaced by overloaded "abs" function;
@@ -55,48 +58,26 @@
Lfp, Gfp, WF); this only affects ML packages that refer to const names
internally;
-* HOL, ZF: syntax for quotienting wrt an equivalence relation changed
-from A/r to A//r;
+* HOL and ZF: syntax for quotienting wrt an equivalence relation
+changed from A/r to A//r;
-* HOL: qed_spec_mp now also removes bounded ALL;
+* ZF: new treatment of arithmetic (nat & int) may break some old
+proofs;
-* ZF: new treatment of arithmetic (nat & int) may break some old proofs;
+* Isar: renamed some attributes (RS -> THEN, simplify -> simplified,
+rulify -> rule_format, elimify -> elim_format, ...);
* Isar/Provers: intro/elim/dest attributes changed; renamed
intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
should have to change intro!! to intro? only); replaced "delrule" by
"rule del";
-* Isar: changed syntax of local blocks from {{ }} to { };
-
-* Isar: renamed 'RS' attribute to 'THEN';
-
-* Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...);
-
* Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
* Provers: strengthened force_tac by using new first_best_tac;
-* Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
- [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
-use instead the strong form,
- [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
-In HOL, FOL and ZF the function cla_make_elim will create such rules
-from destruct-rules;
-
-* Provers: safe_asm_full_simp_tac is no longer in the simplifier signature. Use
- val safe_asm_full_simp_tac = generic_simp_tac true (true,true,true);
- if required.
-
-* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
-timing flag supersedes proof_timing and Toplevel.trace;
-
-* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
-
-* ML: PureThy.add_defs gets additional argument to indicate potential
-overloading (usually false);
-
-* LaTeX: several changes of isabelle.sty;
+* LaTeX document preparation: several changes of isabelle.sty (see
+lib/texinputs);
*** Document preparation ***
@@ -114,7 +95,8 @@
of isatool usedir;
* isatool usedir -D now lets isatool latex -o sty update the Isabelle
-style files, achieving self-contained LaTeX sources;
+style files, achieving self-contained LaTeX sources and simplifying
+LaTeX debugging;
* old-style theories now produce (crude) LaTeX output as well;
@@ -122,139 +104,140 @@
on WWW server seperately); improved graphs of nested sessions; removed
graph for 'all sessions';
-* several improvements in isabelle.sty; \isabellestyle{it} produces
-near math mode output; \isamarkupheader is now \section by default;
+* several improvements in isabelle style files; \isabellestyle{it}
+produces fake math mode output; \isamarkupheader is now \section by
+default; see lib/texinputs/isabelle.sty etc.;
*** Isar ***
-* Pure: local results and corresponding term bindings are now subject
-to Hindley-Milner polymorphism (similar to ML); this accommodates
-incremental type-inference nicely;
+* Isar/Pure: local results and corresponding term bindings are now
+subject to Hindley-Milner polymorphism (similar to ML); this
+accommodates incremental type-inference very nicely;
-* Pure: new derived language element 'obtain' supports generalized
-existence reasoning;
+* Isar/Pure: new derived language element 'obtain' supports
+generalized existence reasoning;
-* Pure: new calculational elements 'moreover' and 'ultimately' support
-accumulation of results, without applying any rules yet;
+* Isar/Pure: new calculational elements 'moreover' and 'ultimately'
+support accumulation of results, without applying any rules yet;
+useful to collect intermediate results without explicit name
+references, and for use with transitivity rules with more than 2
+premises;
-* Pure: scalable support for case-analysis type proofs: new 'case'
-language element refers to local contexts symbolically, as produced by
-certain proof methods; internally, case names are attached to theorems
-as "tags";
+* Isar/Pure: scalable support for case-analysis type proofs: new
+'case' language element refers to local contexts symbolically, as
+produced by certain proof methods; internally, case names are attached
+to theorems as "tags";
-* Pure: theory command 'hide' removes declarations from
+* Isar/Pure: theory command 'hide' removes declarations from
class/type/const name spaces;
-* Pure: theory command 'defs' supports option "(overloaded)" to
+* Isar/Pure: theory command 'defs' supports option "(overloaded)" to
indicate potential overloading;
-* Pure: changed syntax of local blocks from {{ }} to { };
-
-* Pure: renamed 'RS' attribute to 'THEN';
-
-* Pure: syntax of sorts made 'inner', i.e. have to write "{a, b, c}"
-instead of {a, b, c};
-
-* Pure now provides its own version of intro/elim/dest attributes;
-useful for building new logics, but beware of confusion with the
-version in Provers/classical;
+* Isar/Pure: changed syntax of local blocks from {{ }} to { };
-* Pure: the local context of (non-atomic) goals is provided via case
-name 'antecedent';
-
-* Pure: removed obsolete 'transfer' attribute (transfer of thms to the
-current context is now done automatically);
+* Isar/Pure: syntax of sorts made 'inner', i.e. have to write
+"{a,b,c}" instead of {a,b,c};
-* Pure: theory command 'method_setup' provides a simple interface for
-definining proof methods in ML;
-
-* Provers: 'simp' method now supports 'cong' modifiers;
-
-* Provers: hypsubst support; also plain subst and symmetric attribute
-(the latter supercedes [RS sym]);
+* Isar/Pure now provides its own version of intro/elim/dest
+attributes; useful for building new logics, but beware of confusion
+with the version in Provers/classical;
-* Provers: splitter support (via 'split' attribute and 'simp' method
-modifier); 'simp' method: 'only:' modifier removes loopers as well
-(including splits);
-
-* Provers: added 'fastsimp' and 'clarsimp' methods (combination of
-Simplifier and Classical reasoner);
-
-* Provers: added 'arith_split' attribute;
-
-* HOL: new proof method 'cases' and improved version of 'induct' now
-support named cases; major packages (inductive, datatype, primrec,
-recdef) support case names and properly name parameters;
+* Isar/Pure: the local context of (non-atomic) goals is provided via
+case name 'antecedent';
-* HOL: removed 'case_split' thm binding, should use 'cases' proof
-method anyway;
-
-* HOL: removed obsolete expand_if = split_if; theorems if_splits =
-split_if split_if_asm; datatype package provides theorems foo.splits =
-foo.split foo.split_asm for each datatype;
+* Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms
+to the current context is now done automatically);
-* HOL/Calculation: new rules for substitution in inequalities
-(monotonicity conditions are extracted to be proven at end);
+* Isar/Pure: theory command 'method_setup' provides a simple interface
+for definining proof methods in ML;
-* HOL/inductive: rename "intrs" to "intros" (potential
-INCOMPATIBILITY); emulation of mk_cases feature for proof scripts:
-'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
-(simplified)) method in proper proofs;
-
-* Provers: intro/elim/dest attributes changed; renamed
+* Isar/Provers: intro/elim/dest attributes changed; renamed
intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
most cases, one should have to change intro!! to intro? only);
replaced "delrule" by "rule del";
-* names of theorems etc. may be natural numbers as well;
+* Isar/Provers: new 'hypsubst' method, plain 'subst' method and
+'symmetric' attribute (the latter supercedes [RS sym]);
+
+* Isar/Provers: splitter support (via 'split' attribute and 'simp'
+method modifier); 'simp' method: 'only:' modifier removes loopers as
+well (including splits);
+
+* Isar/Provers: Simplifier and Classical methods now support all kind
+of modifiers used in the past, including 'cong', 'iff', etc.
+
+* Isar/Provers: added 'fastsimp' and 'clarsimp' methods (combination
+of Simplifier and Classical reasoner);
+
+* Isar/HOL: new proof method 'cases' and improved version of 'induct'
+now support named cases; major packages (inductive, datatype, primrec,
+recdef) support case names and properly name parameters;
-* 'pr' command: optional arguments for goals_limit and
+* Isar/HOL: new transitivity rules for substitution in inequalities --
+monotonicity conditions are extracted to be proven at end of
+calculations;
+
+* Isar/HOL: removed 'case_split' thm binding, should use 'cases' proof
+method anyway;
+
+* Isar/HOL: removed old expand_if = split_if; theorems if_splits =
+split_if split_if_asm; datatype package provides theorems foo.splits =
+foo.split foo.split_asm for each datatype;
+
+* Isar/HOL: tuned inductive package, rename "intrs" to "intros"
+(potential INCOMPATIBILITY), emulation of mk_cases feature for proof
+scripts: new 'inductive_cases' command and 'ind_cases' method; (Note:
+use "(cases (simplified))" method in proper proof texts);
+
+* Isar/HOL: added global 'arith_split' attribute for 'arith' method;
+
+* Isar: names of theorems etc. may be natural numbers as well;
+
+* Isar: 'pr' command: optional arguments for goals_limit and
ProofContext.prems_limit; no longer prints theory contexts, but only
proof states;
-* diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
+* Isar: diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
additional print modes to be specified; e.g. "pr(latex)" will print
proof state according to the Isabelle LaTeX style;
-* improved support for emulating tactic scripts, including proof
+* Isar: improved support for emulating tactic scripts, including proof
methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac',
'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac'
(for HOL datatypes);
-* simplified (more robust) goal selection of proof methods: 1st goal,
-all goals, or explicit goal specifier (tactic emulation); thus 'proof
-method scripts' have to be in depth-first order;
+* Isar: simplified (more robust) goal selection of proof methods: 1st
+goal, all goals, or explicit goal specifier (tactic emulation); thus
+'proof method scripts' have to be in depth-first order;
-* tuned 'let' syntax: replaced 'as' keyword by 'and';
+* Isar: tuned 'let' syntax: replaced 'as' keyword by 'and';
-* removed 'help' command, which hasn't been too helpful anyway; should
-instead use individual commands for printing items (print_commands,
-print_methods etc.);
+* Isar: removed 'help' command, which hasn't been too helpful anyway;
+should instead use individual commands for printing items
+(print_commands, print_methods etc.);
-* added 'nothing' --- the empty list of theorems;
+* Isar: added 'nothing' --- the empty list of theorems;
*** HOL ***
-* HOL/Lambda: converted into new-style theory and document;
-
* HOL/Algebra: new theory of rings and univariate polynomials, by
Clemens Ballarin;
-* HOL/ex: new theory Factorization proving the Fundamental Theorem of
-Arithmetic, by Thomas M Rasmussen;
-
-* HOL/ex/Multiquote: multiple nested quotations and anti-quotations --
-basically a generalized version of de-Bruijn representation; very
-useful in avoiding lifting of operations;
+* HOL/NumberTheory: Fundamental Theorem of Arithmetic, Chinese
+Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M
+Rasmussen;
-* HOL/NumberTheory: Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's
-Theorem, by Thomas M Rasmussen;
+* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David
+von Oheimb;
-* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog;
+* HOL/Lambda: converted into new-style theory and document;
-* HOL/Real: "rabs" replaced by overloaded "abs" function;
+* HOL/ex/Multiquote: example of multiple nested quotations and
+anti-quotations -- basically a generalized version of de-Bruijn
+representation; very useful in avoiding lifting of operations;
* HOL/record: added general record equality rule to simpset; fixed
select-update simplification procedure to handle extended records as
@@ -266,7 +249,7 @@
* HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.
Types nat and int belong to this axclass;
-* greatly improved simplification involving numerals of type nat, int, real:
+* HOL: greatly improved simplification involving numerals of type nat, int, real:
(i + #8 + j) = Suc k simplifies to #7 + (i + j) = k
i*j + k + j*#3*i simplifies to #4*(i*j) + k
two terms #m*u and #n*u are replaced by #(m+n)*u
@@ -274,9 +257,9 @@
and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
-* HOL: meson_tac is available (previously in ex/meson.ML). It is a powerful
- prover for predicate logic but knows nothing of clasets. For examples of
- what it can do, see ex/mesontest.ML and ex/mesontest2.ML;
+* HOL: meson_tac is available (previously in ex/meson.ML); it is a
+powerful prover for predicate logic but knows nothing of clasets; see
+ex/mesontest.ML and ex/mesontest2.ML for example applications;
* HOL: new version of "case_tac" subsumes both boolean case split and
"exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
@@ -286,7 +269,7 @@
selector expression is simplified, but not the remaining arms. To
enable full simplification of case-expressions for datatype t, you
need to remove t.weak_case_cong from the simpset, either permanently
-(Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
+(Delcongs [thm"t.weak_case_cong"];) or locally (delcongs [...]).
* HOL/recdef: the recursion equations generated by 'recdef' for
function 'f' are now called f.simps instead of f.rules; if all
@@ -300,58 +283,68 @@
provision of a termination measure. The latter is necessary once the
invariant proof rule for while is applied.
-* HOL: new (overloaded) notation for the set of elements below/above some
-element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
+* HOL: new (overloaded) notation for the set of elements below/above
+some element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
* HOL: theorems impI, allI, ballI bound as "strip";
-* new tactic induct_thm_tac: thm -> string -> int -> tactic
+* HOL: new tactic induct_thm_tac: thm -> string -> int -> tactic
induct_tac th "x1 ... xn" expects th to have a conclusion of the form
P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th;
-* new functions rulify/rulify_no_asm: thm -> thm for turning outer
--->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm;
+* HOL/Real: "rabs" replaced by overloaded "abs" function;
-* theory Sexp now in HOL/Induct examples (it used to be part of main
-HOL, but was unused);
+* HOL: theory Sexp now in HOL/Induct examples (it used to be part of
+main HOL, but was unused);
-* fewer consts declared as global (e.g. have to refer to "Lfp.lfp"
-instead of "lfp" internally; affects ML packages only);
+* HOL: fewer consts declared as global (e.g. have to refer to
+"Lfp.lfp" instead of "lfp" internally; affects ML packages only);
-* tuned AST representation of nested pairs, avoiding bogus output in
-case of overlap with user translations (e.g. judgements over tuples);
+* HOL: tuned AST representation of nested pairs, avoiding bogus output
+in case of overlap with user translations (e.g. judgements over
+tuples); (note that the underlying logical represenation is still
+bogus);
*** ZF ***
-* simplification automatically cancels common terms in arithmetic expressions
-over nat and int;
+* ZF: simplification automatically cancels common terms in arithmetic
+expressions over nat and int;
-* new treatment of nat to minimize type-checking: all operators coerce their
-operands to a natural number using the function natify, making the algebraic
-laws unconditional;
-
-* as above, for int: operators coerce their operands to an integer using the
-function intify;
+* ZF: new treatment of nat to minimize type-checking: all operators
+coerce their operands to a natural number using the function natify,
+making the algebraic laws unconditional;
-* the integer library now contains many of the usual laws for the orderings,
-including $<=, and monotonicity laws for $+ and $*;
+* ZF: as above, for int: operators coerce their operands to an integer
+using the function intify;
-* new example ZF/ex/NatSum to demonstrate integer arithmetic simplification;
+* ZF: the integer library now contains many of the usual laws for the
+orderings, including $<=, and monotonicity laws for $+ and $*;
-*** FOL & ZF ***
+* ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic
+simplification;
-* AddIffs now available, giving theorems of the form P<->Q to the
-simplifier and classical reasoner simultaneously;
+* FOL and ZF: AddIffs now available, giving theorems of the form P<->Q
+to the simplifier and classical reasoner simultaneously;
*** General ***
+* Provers: blast_tac now handles actual object-logic rules as
+assumptions; note that auto_tac uses blast_tac internally as well;
+
+* Provers: new functions rulify/rulify_no_asm: thm -> thm for turning
+outer -->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm;
+
* Provers: delrules now handles destruct rules as well (no longer need
explicit make_elim);
-* Provers: blast(_tac) now handles actual object-logic rules as
-assumptions; note that auto(_tac) uses blast(_tac) internally as well;
+* Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
+ [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
+use instead the strong form,
+ [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
+in HOL, FOL and ZF the function cla_make_elim will create such rules
+from destruct-rules;
* Provers: Simplifier.easy_setup provides a fast path to basic
Simplifier setup for new object-logics;
@@ -361,6 +354,10 @@
* Pure: improved name spaces: ambiguous output is qualified; support
for hiding of names;
+* system: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and
+XSYMBOL_HOME; no longer need to do manual configuration in most
+situations;
+
* system: compression of ML heaps images may now be controlled via -c
option of isabelle and isatool usedir (currently only observed by
Poly/ML);
@@ -370,21 +367,20 @@
* system: provide TAGS file for Isabelle sources;
-* settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and
-XSYMBOL_HOME; no longer need to do manual configuration in most
-situations;
-
* ML: infix 'OF' is a version of 'MRS' with more appropriate argument
order;
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
timing flag supersedes proof_timing and Toplevel.trace;
+* ML: new combinators |>> and |>>> for incremental transformations
+with secondary results (e.g. certain theory extensions):
+
* ML: PureThy.add_defs gets additional argument to indicate potential
overloading (usually false);
-* ML: new combinators |>> and |>>> for incremental transformations
-with secondary results (e.g. certain theory extensions):
+* ML: PureThy.add_thms/add_axioms/add_defs now return theorems as
+results;