equal
deleted
inserted
replaced
|
1 (* Title: HOL/Subst/ROOT.ML |
|
2 ID: $Id$ |
|
3 Authors: Martin Coen, Cambridge University Computer Laboratory |
|
4 Konrad Slind, TU Munich |
|
5 Copyright 1993 University of Cambridge, |
|
6 1996 TU Munich |
|
7 |
|
8 Substitution and Unification in Higher-Order Logic. |
|
9 |
|
10 Implements Manna & Waldinger's formalization, with Paulson's simplifications, |
|
11 and some new simplifications by Slind. |
|
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 |
|
18 Setplus - minor additions to HOL's set theory |
|
19 Alist - association lists |
|
20 Uterm - data type of terms |
|
21 Subst - substitutions |
|
22 Unify - specification of unification and conditions for |
|
23 correctness and termination |
|
24 |
|
25 To load, type use"ROOT1.ML"; into an Isabelle-HOL that has TFL |
|
26 also loaded. |
|
27 *) |
|
28 |
|
29 HOL_build_completed; (*Cause examples to fail if HOL did*) |
|
30 |
|
31 writeln"Root file for Substitutions and Unification"; |
|
32 loadpath := "../../" :: !loadpath; (* to get "WF1" *) |
|
33 use_thy "Unify1"; |
|
34 |
|
35 writeln"END: Root file for Substitutions and Unification"; |