src/CCL/ROOT.ML
changeset 32740 9dd0a2f83429
parent 32153 a0e57fb1b930
child 38798 89f273ab1d42
--- a/src/CCL/ROOT.ML	Tue Sep 29 14:59:24 2009 +0200
+++ b/src/CCL/ROOT.ML	Tue Sep 29 16:24:36 2009 +0200
@@ -3,12 +3,11 @@
     Copyright   1993  University of Cambridge
 
 Classical Computational Logic based on First-Order Logic.
+
+A computational logic for an untyped functional language with
+evaluation to weak head-normal form.
 *)
 
-set eta_contract;
-
-(* CCL - a computational logic for an untyped functional language *)
-(*                       with evaluation to weak head-normal form *)
+Unsynchronized.set eta_contract;
 
 use_thys ["Wfd", "Fix"];
-