summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

CHANGES-92f.txt

author | wenzelm |

Tue, 06 Aug 2002 11:19:00 +0200 | |

changeset 13459 | 83f41b047a39 |

parent 0 | a5a9c433f639 |

permissions | -rw-r--r-- |

* Pure: predefined locales "var" and "struct" are useful for sharing
parameters (as in CASL, for example); just specify something like
``var x + var y + struct M'' as import;

**** Isabelle-92f : 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. Classical reasoning (e.g. fast_tac) runs up to 30% faster when large numbers of rules are involved. Rewriting (e.g. SIMP_TAC) runs up to 3 times faster for large subgoals. The new version will not benefit everybody; unless you require greater speed, it may be best to stay with the existing version. The new changes have not been documented properly, and there are a few incompatibilities. THE SPEEDUPS 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.