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