doc-src/CHANGES-93.txt
changeset 103 30bd42401ab2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/CHANGES-93.txt	Tue Nov 09 16:47:38 1993 +0100
@@ -0,0 +1,90 @@
+**** Isabelle-93 : a faster version of Isabelle-92 ****
+
+Isabelle now runs faster through a combination of improvements: pattern
+unification, discrimination nets and removal of assumptions during
+simplification.  A new simplifier, although less flexible than the old one,
+runs many times faster for large subgoals.  Classical reasoning
+(e.g. fast_tac) runs up to 30% faster when large numbers of rules are
+involved.  Incompatibilities are few, and mostly concern the simplifier.
+
+THE SPEEDUPS
+
+The new simplifier is described in the Reference Manual, Chapter 8.  See
+below for advice on converting.
+
+Pattern unification is completely invisible to users.  It efficiently
+handles a common case of higher-order unification.
+
+Discrimination nets replace the old stringtrees.  They provide fast lookup
+in a large set of rules for matching or unification.  New "net" tactics
+replace the "compat_..." tactics based on stringtrees.  Tactics
+biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and
+match_from_net_tac take a net, rather than a list of rules, and perform
+resolution or matching.  Tactics net_biresolve_tac, net_bimatch_tac
+net_resolve_tac and net_match_tac take a list of rules, build a net
+(internally) and perform resolution or matching.
+
+The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a
+list of theorems, has been extended to handle unknowns (although not type
+unknowns).  The simplification tactics now use METAHYPS to economise on
+storage consumption, and to avoid problems involving "parameters" bound in
+a subgoal.  The modified simplifier now requires the auto_tac to take an
+extra argument: a list of theorems, which represents the assumptions of the
+current subgoal.
+
+OTHER CHANGES
+
+Apart from minor improvements in Pure Isabelle, the main other changes are
+extensions to object-logics.  HOL now contains a treatment of co-induction
+and co-recursion, while ZF contains a formalization of equivalence classes,
+the integers and binary arithmetic.  None of this material is documented.
+
+
+CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL)
+
+1.  Run a crude shell script to convert your ML-files:
+
+	change_simp *ML
+
+2.  Most congruence rules are no longer needed.  Hence you should remove all
+calls to mk_congs and mk_typed_congs (they no longer exist) and most
+occurrences of addcongs.  The only exception are congruence rules for special
+constants like (in FOL)
+
+[| ?P <-> ?P'; ?P' ==> ?Q <-> ?Q' |] ==> ?P --> ?Q = ?P' --> ?Q'
+and 
+[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
+(ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
+
+where some of the arguments are simplified under additional premises.  Most
+likely you don't have any constructs like that, or they are already included
+in the basic simpset.
+
+3.  In case you have used the addsplits facilities of the old simplifier:
+The case-splitting and simplification tactics have been separated.  If you
+want to interleave case-splitting with simplification, you have do so
+explicitly by the following command:
+
+ss setloop (split_tac split_thms)
+
+where ss is a simpset and split_thms the list of case-splitting theorems.
+The shell script in step 1 tries to convert to from addsplits to setloop
+automatically.
+
+4.  If you have used setauto, you have to change it to setsolver by hand.
+The solver is more delicate than the auto tactic used to be.  For details see
+the full description of the new simplifier.  One very slight incompatibility
+is the fact that the old auto tactic could sometimes see premises as part of
+the proof state, whereas now they are always passed explicit as arguments.
+
+5.  It is quite likely that a few proofs require further hand massaging.
+
+Known incompatibilities:
+- Applying a rewrite rule cannot instantiate a subgoal.  This rules out
+solving a premise of a conditional rewrite rule with extra unknowns by
+rewriting.  Only the solver can instantiate.
+
+Known bugs:
+- The names of bound variables can be changed by the simplifier.
+
+