--- 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";