CHANGES-92f.txt
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/CHANGES-92f.txt	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,40 @@
     1.4 +**** Isabelle-92f : a faster version of Isabelle-92 ****
     1.5 +
     1.6 +Isabelle now runs faster through a combination of improvements: pattern
     1.7 +unification, discrimination nets and removal of assumptions during
     1.8 +simplification.  Classical reasoning (e.g. fast_tac) runs up to 30% faster
     1.9 +when large numbers of rules are involved.  Rewriting (e.g. SIMP_TAC) runs
    1.10 +up to 3 times faster for large subgoals.  
    1.11 +
    1.12 +The new version will not benefit everybody; unless you require greater
    1.13 +speed, it may be best to stay with the existing version.  The new changes
    1.14 +have not been documented properly, and there are a few incompatibilities.
    1.15 +
    1.16 +THE SPEEDUPS
    1.17 +
    1.18 +Pattern unification is completely invisible to users.  It efficiently
    1.19 +handles a common case of higher-order unification.
    1.20 +
    1.21 +Discrimination nets replace the old stringtrees.  They provide fast lookup
    1.22 +in a large set of rules for matching or unification.  New "net" tactics
    1.23 +replace the "compat_..." tactics based on stringtrees.  Tactics
    1.24 +biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and
    1.25 +match_from_net_tac take a net, rather than a list of rules, and perform
    1.26 +resolution or matching.  Tactics net_biresolve_tac, net_bimatch_tac
    1.27 +net_resolve_tac and net_match_tac take a list of rules, build a net
    1.28 +(internally) and perform resolution or matching.
    1.29 +
    1.30 +The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a
    1.31 +list of theorems, has been extended to handle unknowns (although not type
    1.32 +unknowns).  The simplification tactics now use METAHYPS to economise on
    1.33 +storage consumption, and to avoid problems involving "parameters" bound in
    1.34 +a subgoal.  The modified simplifier now requires the auto_tac to take an
    1.35 +extra argument: a list of theorems, which represents the assumptions of the
    1.36 +current subgoal.
    1.37 +
    1.38 +OTHER CHANGES
    1.39 +
    1.40 +Apart from minor improvements in Pure Isabelle, the main other changes are
    1.41 +extensions to object-logics.  HOL now contains a treatment of co-induction
    1.42 +and co-recursion, while ZF contains a formalization of equivalence classes,
    1.43 +the integers and binary arithmetic.  None of this material is documented.