CHANGES-92f.txt
author lcp
Wed, 15 Mar 1995 10:56:39 +0100
changeset 955 aa0c5f9daf5b
parent 0 a5a9c433f639
permissions -rw-r--r--
Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
**** Isabelle-92f : a faster version of Isabelle-92 ****
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
Isabelle now runs faster through a combination of improvements: pattern
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
unification, discrimination nets and removal of assumptions during
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
simplification.  Classical reasoning (e.g. fast_tac) runs up to 30% faster
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
when large numbers of rules are involved.  Rewriting (e.g. SIMP_TAC) runs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
up to 3 times faster for large subgoals.  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
The new version will not benefit everybody; unless you require greater
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
speed, it may be best to stay with the existing version.  The new changes
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
have not been documented properly, and there are a few incompatibilities.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
THE SPEEDUPS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
Pattern unification is completely invisible to users.  It efficiently
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
handles a common case of higher-order unification.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
Discrimination nets replace the old stringtrees.  They provide fast lookup
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
in a large set of rules for matching or unification.  New "net" tactics
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
replace the "compat_..." tactics based on stringtrees.  Tactics
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
match_from_net_tac take a net, rather than a list of rules, and perform
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
resolution or matching.  Tactics net_biresolve_tac, net_bimatch_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
net_resolve_tac and net_match_tac take a list of rules, build a net
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
(internally) and perform resolution or matching.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
list of theorems, has been extended to handle unknowns (although not type
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
unknowns).  The simplification tactics now use METAHYPS to economise on
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
storage consumption, and to avoid problems involving "parameters" bound in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a subgoal.  The modified simplifier now requires the auto_tac to take an
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
extra argument: a list of theorems, which represents the assumptions of the
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
current subgoal.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
OTHER CHANGES
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
Apart from minor improvements in Pure Isabelle, the main other changes are
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
extensions to object-logics.  HOL now contains a treatment of co-induction
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
and co-recursion, while ZF contains a formalization of equivalence classes,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
the integers and binary arithmetic.  None of this material is documented.