src/CCL/ROOT.ML
changeset 121 d392174734e9
parent 72 099d949fe467
child 997 a58082b8066c
equal deleted inserted replaced
120:09287f26bfb8 121:d392174734e9
     9 val banner = "Classical Computational Logic (in FOL)";
     9 val banner = "Classical Computational Logic (in FOL)";
    10 
    10 
    11 (* Higher-Order Set Theory Extension to FOL *)
    11 (* Higher-Order Set Theory Extension to FOL *)
    12 (*      used as basis for CCL               *)
    12 (*      used as basis for CCL               *)
    13 
    13 
    14 set_loadpath [".", "../FOL"];
    14 use_thy "Set";
    15 
       
    16 use_thy "set";
       
    17 use     "subset.ML";
    15 use     "subset.ML";
    18 use     "equalities.ML";
    16 use     "equalities.ML";
    19 use     "mono.ML";
    17 use     "mono.ML";
    20 use_thy "lfp";
    18 use_thy "Lfp";
    21 use_thy "gfp";
    19 use_thy "Gfp";
    22 
    20 
    23 (* CCL - a computational logic for an untyped functional language *)
    21 (* CCL - a computational logic for an untyped functional language *)
    24 (*                       with evaluation to weak head-normal form *)
    22 (*                       with evaluation to weak head-normal form *)
    25 
    23 
    26 use_thy "ccl";
    24 use_thy "CCL";
    27 use_thy "term";
    25 use_thy "Term";
    28 use_thy "type";
    26 use_thy "Type";
    29 use     "coinduction.ML";
    27 use     "coinduction.ML";
    30 use_thy "hered";
    28 use_thy "Hered";
    31 
    29 
    32 use_thy "trancl";
    30 use_thy "Trancl";
    33 use_thy "wfd";
    31 use_thy "Wfd";
    34 use     "genrec.ML";
    32 use     "genrec.ML";
    35 use     "typecheck.ML";
    33 use     "typecheck.ML";
    36 use     "eval.ML";
    34 use     "eval.ML";
    37 use_thy "fix";
    35 use_thy "Fix";
    38 
    36 
    39 val CCL_build_completed = ();   (*indicate successful build*)
    37 val CCL_build_completed = ();   (*indicate successful build*)