author | wenzelm |
Wed, 31 Dec 1997 15:17:49 +0100 | |
changeset 4504 | 2f39aa4bebf3 |
parent 3192 | a75558a4ed37 |
child 6349 | f7750d816c21 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Subst/ROOT.ML |
1266 | 2 |
ID: $Id$ |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
3 |
Authors: Martin Coen, Cambridge University Computer Laboratory |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
4 |
Konrad Slind, TU Munich |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
5 |
Copyright 1993 University of Cambridge, |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
6 |
1996 TU Munich |
968 | 7 |
|
8 |
Substitution and Unification in Higher-Order Logic. |
|
9 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
10 |
Implements Manna & Waldinger's formalization, with Paulson's simplifications, |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
11 |
and some new simplifications by Slind. |
968 | 12 |
|
13 |
Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm. |
|
14 |
SCP 1 (1981), 5-48 |
|
15 |
||
16 |
L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170 |
|
17 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
18 |
AList - association lists |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
19 |
UTerm - data type of terms |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
20 |
Subst - substitutions |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
21 |
Unifier - specification of unification and conditions for |
968 | 22 |
correctness and termination |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
23 |
Unify - the unification function |
968 | 24 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
25 |
To load, type use"ROOT.ML"; into an Isabelle-HOL that has TFL |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
26 |
also loaded. |
968 | 27 |
*) |
28 |
||
1165 | 29 |
HOL_build_completed; (*Cause examples to fail if HOL did*) |
968 | 30 |
|
31 |
writeln"Root file for Substitutions and Unification"; |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
32 |
use_thy "Unify"; |
968 | 33 |
|
34 |
writeln"END: Root file for Substitutions and Unification"; |