# HG changeset patch
# User nipkow
# Date 801151226 -7200
# Node ID 50ac36140e21801f4a2230623c9f2c9a4fe0f4e6
# Parent  13a3df2adbe52a7be01d8fcd15307be2f1ae744d
Moved comment from ParRed.thy to ROOT.ML

diff -r 13a3df2adbe5 -r 50ac36140e21 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Mon May 22 15:58:57 1995 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Mon May 22 16:00:26 1995 +0200
@@ -4,11 +4,6 @@
     Copyright   1995 TU Muenchen
 
 Parallel reduction and a complete developments function "cd".
-Follows the first two pages of
-
-@article{Takahashi-IC-95,author="Masako Takahashi",
-title="Parallel Reductions in $\lambda$-Calculus",
-journal=IC,year=1995,volume=118,pages="120--127"}
 *)
 
 ParRed = Lambda + Confluence +
diff -r 13a3df2adbe5 -r 50ac36140e21 src/HOL/Lambda/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ROOT.ML	Mon May 22 16:00:26 1995 +0200
@@ -0,0 +1,19 @@
+(*  Title: 	CHOL/IMP/ROOT.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1995 TUM
+
+Confluence proof for untyped lambda-calculus using de Bruijn's notation.
+Extremely slick proof; follows the first two pages of
+
+@article{Takahashi-IC-95,author="Masako Takahashi",
+title="Parallel Reductions in $\lambda$-Calculus",
+journal=IC,year=1995,volume=118,pages="120--127"}
+
+*)
+
+CHOL_build_completed;	(*Make examples fail if CHOL did*)
+
+writeln"Root file for CHOL/Lambda";
+loadpath := [".","Lambda"];
+time_use_thy "ParRed";