**** Isabelle-92f : a faster version of Isabelle-92 ****Isabelle now runs faster through a combination of improvements: patternunification, discrimination nets and removal of assumptions duringsimplification. Classical reasoning (e.g. fast_tac) runs up to 30% fasterwhen large numbers of rules are involved. Rewriting (e.g. SIMP_TAC) runsup to 3 times faster for large subgoals. The new version will not benefit everybody; unless you require greaterspeed, it may be best to stay with the existing version. The new changeshave not been documented properly, and there are a few incompatibilities.THE SPEEDUPSPattern unification is completely invisible to users. It efficientlyhandles a common case of higher-order unification.Discrimination nets replace the old stringtrees. They provide fast lookupin a large set of rules for matching or unification. New "net" tacticsreplace the "compat_..." tactics based on stringtrees. Tacticsbiresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac andmatch_from_net_tac take a net, rather than a list of rules, and performresolution or matching. Tactics net_biresolve_tac, net_bimatch_tacnet_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 alist of theorems, has been extended to handle unknowns (although not typeunknowns). The simplification tactics now use METAHYPS to economise onstorage consumption, and to avoid problems involving "parameters" bound ina subgoal. The modified simplifier now requires the auto_tac to take anextra argument: a list of theorems, which represents the assumptions of thecurrent subgoal.OTHER CHANGESApart from minor improvements in Pure Isabelle, the main other changes areextensions to object-logics. HOL now contains a treatment of co-inductionand co-recursion, while ZF contains a formalization of equivalence classes,the integers and binary arithmetic. None of this material is documented.