TFL/sys.sml
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 4062 fa2eb95b1b2d
child 6498 1ebbe18fe236
permissions -rw-r--r--
adapted extend_trfunsT;
paulson@3353
     1
(*  Title:      TFL/sys
paulson@3302
     2
    ID:         $Id$
paulson@3302
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
paulson@3302
     4
    Copyright   1997  University of Cambridge
paulson@3302
     5
paulson@3302
     6
Compile the TFL system
paulson@3302
     7
*)
paulson@2112
     8
paulson@2112
     9
(* Portability stuff *)
paulson@2112
    10
nonfix prefix;
paulson@2112
    11
paulson@2112
    12
(* Establish a base of common and/or helpful functions. *)
paulson@2112
    13
use "utils.sig";
paulson@2112
    14
paulson@2112
    15
use "usyntax.sig";
paulson@2112
    16
use "rules.sig";
paulson@2112
    17
use "thry.sig";
paulson@2112
    18
use "thms.sig";
paulson@2112
    19
use "tfl.sig";
paulson@3245
    20
use "utils.sml";
paulson@2112
    21
paulson@2112
    22
(*----------------------------------------------------------------------------
paulson@2112
    23
 *      Supply implementations
paulson@2112
    24
 *---------------------------------------------------------------------------*)
paulson@2112
    25
paulson@2112
    26
use "usyntax.sml";
paulson@2112
    27
use "thms.sml";
paulson@4062
    28
use "dcterm.sml"; 
paulson@4062
    29
use "rules.new.sml";
paulson@2112
    30
use "thry.sml";
paulson@2112
    31
paulson@2112
    32
paulson@2112
    33
(*----------------------------------------------------------------------------
paulson@2112
    34
 *      Link system and specialize for Isabelle 
paulson@2112
    35
 *---------------------------------------------------------------------------*)
paulson@3391
    36
use "tfl.sml";
paulson@4062
    37
use "post.sml";