equal
deleted
inserted
replaced
1 (* Title: HOL/Subst |
1 (* Title: Old_HOL/Subst/ROOT.ML |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Copyright 1993 University of Cambridge |
3 Copyright 1993 University of Cambridge |
4 |
4 |
5 Substitution and Unification in Higher-Order Logic. |
5 Substitution and Unification in Higher-Order Logic. |
6 |
6 |
33 use_thy "Subst/UTLemmas"; |
33 use_thy "Subst/UTLemmas"; |
34 |
34 |
35 use_thy "Subst/Subst"; |
35 use_thy "Subst/Subst"; |
36 use_thy "Subst/Unifier"; |
36 use_thy "Subst/Unifier"; |
37 writeln"END: Root file for Substitutions and Unification"; |
37 writeln"END: Root file for Substitutions and Unification"; |
|
38 |
|
39 make_chart (); (*make HTML chart*) |