TFL/sys.sml
author paulson
Tue, 03 Jun 1997 11:08:08 +0200
changeset 3391 5e45dd3b64e9
parent 3353 9112a2efb9a3
child 4062 fa2eb95b1b2d
permissions -rw-r--r--
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const Changed the TFL functor to a structure (currently called Prim)

(*  Title:      TFL/sys
    ID:         $Id$
    Author:     Konrad Slind, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

Compile the TFL system
*)

(* Portability stuff *)
nonfix prefix;

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

use "usyntax.sig";
use "rules.sig";
use "thry.sig";
use "thms.sig";
use "tfl.sig";
use "utils.sml";

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

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


(*----------------------------------------------------------------------------
 *      Link system and specialize for Isabelle 
 *---------------------------------------------------------------------------*)
use "tfl.sml";
use"post.sml";