--- a/src/HOL/IMP/ROOT.ML Thu Jun 29 12:34:16 1995 +0200
+++ b/src/HOL/IMP/ROOT.ML Thu Jun 29 12:48:48 1995 +0200
@@ -1,4 +1,4 @@
-(* Title: CHOL/IMP/ROOT.ML
+(* Title: HOL/IMP/ROOT.ML
ID: $Id$
Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
Copyright 1995 TUM
@@ -14,9 +14,9 @@
*)
-CHOL_build_completed; (*Make examples fail if CHOL did*)
+HOL_build_completed; (*Make examples fail if HOL did*)
-writeln"Root file for CHOL/IMP";
+writeln"Root file for HOL/IMP";
proof_timing := true;
loadpath := [".","IMP"];
time_use_thy "Properties";
--- a/src/HOL/Integ/ROOT.ML Thu Jun 29 12:34:16 1995 +0200
+++ b/src/HOL/Integ/ROOT.ML Thu Jun 29 12:48:48 1995 +0200
@@ -1,12 +1,12 @@
-(* Title: CHOL/Integ/ROOT
+(* Title: HOL/Integ/ROOT
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
-The Integers in CHOL (ported from ZF by Riccardo Mattolini)
+The Integers in HOL (ported from ZF by Riccardo Mattolini)
*)
-CHOL_build_completed; (*Cause examples to fail if CHOL did*)
+HOL_build_completed; (*Cause examples to fail if HOL did*)
loadpath := ["Integ"];
time_use_thy "Integ";
--- a/src/HOL/Lambda/ROOT.ML Thu Jun 29 12:34:16 1995 +0200
+++ b/src/HOL/Lambda/ROOT.ML Thu Jun 29 12:48:48 1995 +0200
@@ -1,4 +1,4 @@
-(* Title: CHOL/IMP/ROOT.ML
+(* Title: HOL/IMP/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TUM
@@ -12,8 +12,8 @@
*)
-CHOL_build_completed; (*Make examples fail if CHOL did*)
+HOL_build_completed; (*Make examples fail if HOL did*)
-writeln"Root file for CHOL/Lambda";
+writeln"Root file for HOL/Lambda";
loadpath := [".","Lambda"];
time_use_thy "ParRed";
--- a/src/HOL/ROOT.ML Thu Jun 29 12:34:16 1995 +0200
+++ b/src/HOL/ROOT.ML Thu Jun 29 12:48:48 1995 +0200
@@ -86,4 +86,4 @@
init_pps ();
print_depth 8;
-val CHOL_build_completed = (); (*indicate successful build*)
+val HOL_build_completed = (); (*indicate successful build*)
--- a/src/HOL/Subst/ROOT.ML Thu Jun 29 12:34:16 1995 +0200
+++ b/src/HOL/Subst/ROOT.ML Thu Jun 29 12:48:48 1995 +0200
@@ -1,4 +1,4 @@
-(* Title: CHOL/Subst
+(* Title: HOL/Subst
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -22,7 +22,7 @@
To load, go to the parent directory and type use"Subst/ROOT.ML";
*)
-CHOL_build_completed; (*Cause examples to fail if CHOL did*)
+HOL_build_completed; (*Cause examples to fail if HOL did*)
writeln"Root file for Substitutions and Unification";
loadpath := ["Subst"];
--- a/src/HOL/ex/ROOT.ML Thu Jun 29 12:34:16 1995 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Jun 29 12:48:48 1995 +0200
@@ -1,4 +1,4 @@
-(* Title: CHOL/ex/ROOT
+(* Title: HOL/ex/ROOT
ID: $Id$
Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -6,9 +6,9 @@
Executes miscellaneous examples for Higher-Order Logic.
*)
-CHOL_build_completed; (*Cause examples to fail if CHOL did*)
+HOL_build_completed; (*Cause examples to fail if HOL did*)
-writeln "Root file for CHOL examples";
+writeln "Root file for HOL examples";
proof_timing := true;
loadpath := ["ex"];
time_use "ex/cla.ML";
@@ -28,4 +28,4 @@
time_use_thy "Term";
time_use_thy "Simult";
time_use_thy "MT";
-writeln "END: Root file for CHOL examples";
+writeln "END: Root file for HOL examples";