clasohm@0: **** Isabelle-92f : a faster version of Isabelle-92 ****
clasohm@0: 
clasohm@0: Isabelle now runs faster through a combination of improvements: pattern
clasohm@0: unification, discrimination nets and removal of assumptions during
clasohm@0: simplification.  Classical reasoning (e.g. fast_tac) runs up to 30% faster
clasohm@0: when large numbers of rules are involved.  Rewriting (e.g. SIMP_TAC) runs
clasohm@0: up to 3 times faster for large subgoals.  
clasohm@0: 
clasohm@0: The new version will not benefit everybody; unless you require greater
clasohm@0: speed, it may be best to stay with the existing version.  The new changes
clasohm@0: have not been documented properly, and there are a few incompatibilities.
clasohm@0: 
clasohm@0: THE SPEEDUPS
clasohm@0: 
clasohm@0: Pattern unification is completely invisible to users.  It efficiently
clasohm@0: handles a common case of higher-order unification.
clasohm@0: 
clasohm@0: Discrimination nets replace the old stringtrees.  They provide fast lookup
clasohm@0: in a large set of rules for matching or unification.  New "net" tactics
clasohm@0: replace the "compat_..." tactics based on stringtrees.  Tactics
clasohm@0: biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and
clasohm@0: match_from_net_tac take a net, rather than a list of rules, and perform
clasohm@0: resolution or matching.  Tactics net_biresolve_tac, net_bimatch_tac
clasohm@0: net_resolve_tac and net_match_tac take a list of rules, build a net
clasohm@0: (internally) and perform resolution or matching.
clasohm@0: 
clasohm@0: The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a
clasohm@0: list of theorems, has been extended to handle unknowns (although not type
clasohm@0: unknowns).  The simplification tactics now use METAHYPS to economise on
clasohm@0: storage consumption, and to avoid problems involving "parameters" bound in
clasohm@0: a subgoal.  The modified simplifier now requires the auto_tac to take an
clasohm@0: extra argument: a list of theorems, which represents the assumptions of the
clasohm@0: current subgoal.
clasohm@0: 
clasohm@0: OTHER CHANGES
clasohm@0: 
clasohm@0: Apart from minor improvements in Pure Isabelle, the main other changes are
clasohm@0: extensions to object-logics.  HOL now contains a treatment of co-induction
clasohm@0: and co-recursion, while ZF contains a formalization of equivalence classes,
clasohm@0: the integers and binary arithmetic.  None of this material is documented.