TFL/sys.sml
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
(* Compile the TFL system *)
paulson@2112
     2
paulson@2112
     3
(* Portability stuff *)
paulson@2112
     4
nonfix prefix;
paulson@2112
     5
use"mask.sig";
paulson@2112
     6
use"mask.sml";
paulson@2112
     7
paulson@2112
     8
(* Establish a base of common and/or helpful functions. *)
paulson@2112
     9
use "utils.sig";
paulson@2112
    10
use "utils.sml";
paulson@2112
    11
paulson@2112
    12
(* Get the specifications - these are independent of any system *)
paulson@2112
    13
use "usyntax.sig";
paulson@2112
    14
use "rules.sig";
paulson@2112
    15
use "thry.sig";
paulson@2112
    16
use "thms.sig";
paulson@2112
    17
use "tfl.sig";
paulson@2112
    18
paulson@2112
    19
(*----------------------------------------------------------------------------
paulson@2112
    20
 * Load the TFL functor - this is defined totally in terms of the 
paulson@2112
    21
 * above interfaces.
paulson@2112
    22
 *---------------------------------------------------------------------------*)
paulson@2112
    23
paulson@2112
    24
use "tfl.sml";
paulson@2112
    25
paulson@2112
    26
structure Utils = UTILS(val int_to_string = string_of_int);
paulson@2112
    27
paulson@2112
    28
(*----------------------------------------------------------------------------
paulson@2112
    29
 *      Supply implementations
paulson@2112
    30
 *---------------------------------------------------------------------------*)
paulson@2112
    31
paulson@2112
    32
val _ = use_thy"WF1";          (* Wellfoundedness theory *)
paulson@2112
    33
paulson@2112
    34
use "usyntax.sml";
paulson@2112
    35
use "thms.sml";
paulson@2112
    36
use"dcterm.sml"; use"rules.new.sml";
paulson@2112
    37
use "thry.sml";
paulson@2112
    38
paulson@2112
    39
paulson@2112
    40
(*----------------------------------------------------------------------------
paulson@2112
    41
 *      Link system and specialize for Isabelle 
paulson@2112
    42
 *---------------------------------------------------------------------------*)
paulson@2112
    43
structure Prim = TFL(structure Rules = FastRules 
paulson@2112
    44
                     structure Thms  = Thms
paulson@2112
    45
                     structure Thry  = Thry);
paulson@2112
    46
paulson@2112
    47
use"post.sml";
paulson@2112
    48