src/CCL/ROOT.ML
changeset 24106 f2965bf954dc
parent 20140 98acc6d0fab6
child 32153 a0e57fb1b930
equal deleted inserted replaced
24105:af364e2b4048 24106:f2965bf954dc
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Classical Computational Logic based on First-Order Logic.
     6 Classical Computational Logic based on First-Order Logic.
     7 *)
     7 *)
     8 
     8 
     9 val banner = "Classical Computational Logic (in FOL)";
       
    10 writeln banner;
       
    11 
       
    12 set eta_contract;
     9 set eta_contract;
    13 
    10 
    14 (* CCL - a computational logic for an untyped functional language *)
    11 (* CCL - a computational logic for an untyped functional language *)
    15 (*                       with evaluation to weak head-normal form *)
    12 (*                       with evaluation to weak head-normal form *)
    16 
    13 
    17 use_thy "Wfd";
    14 use_thys ["Wfd", "Fix"];
    18 use_thy "Fix";
    15