TFL/sys.sml

+(* 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";
+