TFL/sys.sml
changeset 3191 14bd6e5985f1
parent 2112 3902e9af752f
child 3245 241838c01caf
equal deleted inserted replaced
3190:5aa3756a4bf2 3191:14bd6e5985f1
    27 
    27 
    28 (*----------------------------------------------------------------------------
    28 (*----------------------------------------------------------------------------
    29  *      Supply implementations
    29  *      Supply implementations
    30  *---------------------------------------------------------------------------*)
    30  *---------------------------------------------------------------------------*)
    31 
    31 
    32 val _ = use_thy"WF1";          (* Wellfoundedness theory *)
    32 (* Ignore "Time" exception raised at end of building theory. *)
    33 
       
    34 use "usyntax.sml";
    33 use "usyntax.sml";
    35 use "thms.sml";
    34 use "thms.sml";
    36 use"dcterm.sml"; use"rules.new.sml";
    35 use"dcterm.sml"; use"rules.new.sml";
    37 use "thry.sml";
    36 use "thry.sml";
    38 
    37 
    43 structure Prim = TFL(structure Rules = FastRules 
    42 structure Prim = TFL(structure Rules = FastRules 
    44                      structure Thms  = Thms
    43                      structure Thms  = Thms
    45                      structure Thry  = Thry);
    44                      structure Thry  = Thry);
    46 
    45 
    47 use"post.sml";
    46 use"post.sml";
    48