the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
re-renamed mk_meta_eq_simp to mk_meta_eq
added Eps_eq to simpset
(* 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";