# HG changeset patch
# User clasohm
# Date 804422928 -7200
# Node ID 97b2bb5d43c3cf3c33c4d7c000d93b6e9b5f656f
# Parent  8e969adf64d6afb3f196465678cf56df26f27768
renamed CHOL to HOL

diff -r 8e969adf64d6 -r 97b2bb5d43c3 src/HOL/IMP/ROOT.ML
--- 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";
diff -r 8e969adf64d6 -r 97b2bb5d43c3 src/HOL/Integ/ROOT.ML
--- 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";
diff -r 8e969adf64d6 -r 97b2bb5d43c3 src/HOL/Lambda/ROOT.ML
--- 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";
diff -r 8e969adf64d6 -r 97b2bb5d43c3 src/HOL/ROOT.ML
--- 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*)
diff -r 8e969adf64d6 -r 97b2bb5d43c3 src/HOL/Subst/ROOT.ML
--- 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"];
diff -r 8e969adf64d6 -r 97b2bb5d43c3 src/HOL/ex/ROOT.ML
--- 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";