TFL/tfl.sml
changeset 9878 b145613939c1
parent 9866 90cbf68b9227
child 10015 8c16ec5ba62b
equal deleted inserted replaced
9877:b2a62260f8ac 9878:b145613939c1
    46 
    46 
    47 open BasisLibrary;
    47 open BasisLibrary;
    48 
    48 
    49 structure R = Rules;
    49 structure R = Rules;
    50 structure S = USyntax;
    50 structure S = USyntax;
    51 structure U = S.Utils;
    51 structure U = Utils;
    52 
    52 
    53 
    53 
    54 fun TFL_ERR {func, mesg} = U.ERR {module = "Tfl", func = func, mesg = mesg};
    54 fun TFL_ERR {func, mesg} = U.ERR {module = "Tfl", func = func, mesg = mesg};
    55 
    55 
    56 val concl = #2 o R.dest_thm;
    56 val concl = #2 o R.dest_thm;