TFL/sys.sml
changeset 3391 5e45dd3b64e9
parent 3353 9112a2efb9a3
child 4062 fa2eb95b1b2d
equal deleted inserted replaced
3390:0c7625196d95 3391:5e45dd3b64e9
    10 nonfix prefix;
    10 nonfix prefix;
    11 
    11 
    12 (* Establish a base of common and/or helpful functions. *)
    12 (* Establish a base of common and/or helpful functions. *)
    13 use "utils.sig";
    13 use "utils.sig";
    14 
    14 
    15 (* Get the specifications - these are independent of any system *)
       
    16 use "usyntax.sig";
    15 use "usyntax.sig";
    17 use "rules.sig";
    16 use "rules.sig";
    18 use "thry.sig";
    17 use "thry.sig";
    19 use "thms.sig";
    18 use "thms.sig";
    20 use "tfl.sig";
    19 use "tfl.sig";
    21 
       
    22 (*----------------------------------------------------------------------------
       
    23  * Load the TFL functor - this is defined totally in terms of the 
       
    24  * above interfaces.
       
    25  *---------------------------------------------------------------------------*)
       
    26 
       
    27 use "tfl.sml";
       
    28 
       
    29 use "utils.sml";
    20 use "utils.sml";
    30 
    21 
    31 (*----------------------------------------------------------------------------
    22 (*----------------------------------------------------------------------------
    32  *      Supply implementations
    23  *      Supply implementations
    33  *---------------------------------------------------------------------------*)
    24  *---------------------------------------------------------------------------*)
    40 
    31 
    41 
    32 
    42 (*----------------------------------------------------------------------------
    33 (*----------------------------------------------------------------------------
    43  *      Link system and specialize for Isabelle 
    34  *      Link system and specialize for Isabelle 
    44  *---------------------------------------------------------------------------*)
    35  *---------------------------------------------------------------------------*)
    45 structure Prim = TFL(structure Rules = FastRules 
    36 use "tfl.sml";
    46                      structure Thms  = Thms
       
    47                      structure Thry  = Thry);
       
    48 
       
    49 use"post.sml";
    37 use"post.sml";