TFL/sys.sml
changeset 3245 241838c01caf
parent 3191 14bd6e5985f1
child 3302 404fe31fd8d2
equal deleted inserted replaced
3244:71b760618f30 3245:241838c01caf
     5 use"mask.sig";
     5 use"mask.sig";
     6 use"mask.sml";
     6 use"mask.sml";
     7 
     7 
     8 (* Establish a base of common and/or helpful functions. *)
     8 (* Establish a base of common and/or helpful functions. *)
     9 use "utils.sig";
     9 use "utils.sig";
    10 use "utils.sml";
       
    11 
    10 
    12 (* Get the specifications - these are independent of any system *)
    11 (* Get the specifications - these are independent of any system *)
    13 use "usyntax.sig";
    12 use "usyntax.sig";
    14 use "rules.sig";
    13 use "rules.sig";
    15 use "thry.sig";
    14 use "thry.sig";
    21  * above interfaces.
    20  * above interfaces.
    22  *---------------------------------------------------------------------------*)
    21  *---------------------------------------------------------------------------*)
    23 
    22 
    24 use "tfl.sml";
    23 use "tfl.sml";
    25 
    24 
    26 structure Utils = UTILS(val int_to_string = string_of_int);
    25 use "utils.sml";
    27 
    26 
    28 (*----------------------------------------------------------------------------
    27 (*----------------------------------------------------------------------------
    29  *      Supply implementations
    28  *      Supply implementations
    30  *---------------------------------------------------------------------------*)
    29  *---------------------------------------------------------------------------*)
    31 
    30 
    32 (* Ignore "Time" exception raised at end of building theory. *)
       
    33 use "usyntax.sml";
    31 use "usyntax.sml";
    34 use "thms.sml";
    32 use "thms.sml";
    35 use"dcterm.sml"; use"rules.new.sml";
    33 use"dcterm.sml"; 
       
    34 use"rules.new.sml";
    36 use "thry.sml";
    35 use "thry.sml";
    37 
    36 
    38 
    37 
    39 (*----------------------------------------------------------------------------
    38 (*----------------------------------------------------------------------------
    40  *      Link system and specialize for Isabelle 
    39  *      Link system and specialize for Isabelle