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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     1
(* Compile the TFL system *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     2
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     3
(* Portability stuff *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     4
nonfix prefix;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     5
use"mask.sig";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     6
use"mask.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     7
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     8
(* Establish a base of common and/or helpful functions. *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     9
use "utils.sig";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
use "utils.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
(* Get the specifications - these are independent of any system *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
use "usyntax.sig";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
use "rules.sig";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
use "thry.sig";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
use "thms.sig";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
use "tfl.sig";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    18
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
(*----------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
 * Load the TFL functor - this is defined totally in terms of the 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    21
 * above interfaces.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    22
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
use "tfl.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
structure Utils = UTILS(val int_to_string = string_of_int);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
(*----------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    29
 *      Supply implementations
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    30
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    31
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
val _ = use_thy"WF1";          (* Wellfoundedness theory *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    33
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    34
use "usyntax.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    35
use "thms.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    36
use"dcterm.sml"; use"rules.new.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
use "thry.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    38
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    39
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    40
(*----------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    41
 *      Link system and specialize for Isabelle 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    42
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    43
structure Prim = TFL(structure Rules = FastRules 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    44
                     structure Thms  = Thms
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    45
                     structure Thry  = Thry);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    46
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    47
use"post.sml";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    48