removed LocalTheory.defs, use plain LocalTheory.def;
**** Isabelle-93 : a faster version of Isabelle-92 ****Isabelle now runs faster through a combination of improvements: patternunification, discrimination nets and removal of assumptions duringsimplification. 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 areinvolved. Incompatibilities are few, and mostly concern the simplifier.THE SPEEDUPSThe new simplifier is described in the Reference Manual, Chapter 8. Seebelow for advice on converting.Pattern 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.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 *ML2. Most congruence rules are no longer needed. Hence you should remove allcalls to mk_congs and mk_typed_congs (they no longer exist) and mostoccurrences of addcongs. The only exception are congruence rules for specialconstants 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. Mostlikely you don't have any constructs like that, or they are already includedin 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 youwant to interleave case-splitting with simplification, you have do soexplicitly 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 setloopautomatically.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 seethe full description of the new simplifier. One very slight incompatibilityis the fact that the old auto tactic could sometimes see premises as part ofthe 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 outsolving a premise of a conditional rewrite rule with extra unknowns byrewriting. Only the solver can instantiate.Known bugs:- The names of bound variables can be changed by the simplifier.