diff -r 12943ab62cc5 -r b6c0407f203e Integ/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Integ/ROOT.ML	Mon Feb 27 16:46:38 1995 +0100
@@ -0,0 +1,12 @@
+(*  Title:  	HOL/Integ/ROOT
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+The Integers in HOL (ported from ZF by Riccardo Mattolini)
+*)
+
+HOL_build_completed;    (*Cause examples to fail if HOL did*)
+
+loadpath := ["Integ"];
+time_use_thy "Integ" handle _ => exit 1;