TFL/sys.sml
author wenzelm
Tue, 10 Dec 1996 13:03:44 +0100
changeset 2367 eba760ebe315
parent 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
fixed pris of binder syntax;

(* Compile the TFL system *)

(* Portability stuff *)
nonfix prefix;
use"mask.sig";
use"mask.sml";

(* Establish a base of common and/or helpful functions. *)
use "utils.sig";
use "utils.sml";

(* Get the specifications - these are independent of any system *)
use "usyntax.sig";
use "rules.sig";
use "thry.sig";
use "thms.sig";
use "tfl.sig";

(*----------------------------------------------------------------------------
 * Load the TFL functor - this is defined totally in terms of the 
 * above interfaces.
 *---------------------------------------------------------------------------*)

use "tfl.sml";

structure Utils = UTILS(val int_to_string = string_of_int);

(*----------------------------------------------------------------------------
 *      Supply implementations
 *---------------------------------------------------------------------------*)

val _ = use_thy"WF1";          (* Wellfoundedness theory *)

use "usyntax.sml";
use "thms.sml";
use"dcterm.sml"; use"rules.new.sml";
use "thry.sml";


(*----------------------------------------------------------------------------
 *      Link system and specialize for Isabelle 
 *---------------------------------------------------------------------------*)
structure Prim = TFL(structure Rules = FastRules 
                     structure Thms  = Thms
                     structure Thry  = Thry);

use"post.sml";