# HG changeset patch
# User wenzelm
# Date 968172749 -7200
# Node ID 9a39eabfa17b6f72dd1080884c1f3b493f02a62a
# Parent  b4a170f7d658ac5c89ea39f9ef164b80874b54c3
eliminated;

diff -r b4a170f7d658 -r 9a39eabfa17b TFL/rules.sig
--- a/TFL/rules.sig	Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-(*  Title:      TFL/rules
-    ID:         $Id$
-    Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-Emulation of HOL inference rules for TFL
-*)
-
-signature Rules_sig =
-sig
-(*  structure USyntax : USyntax_sig *)
-  val dest_thm : thm -> term list * term
-
-  (* Inference rules *)
-  val REFL      :cterm -> thm
-  val ASSUME    :cterm -> thm
-  val MP        :thm -> thm -> thm
-  val MATCH_MP  :thm -> thm -> thm
-  val CONJUNCT1 :thm -> thm
-  val CONJUNCT2 :thm -> thm
-  val CONJUNCTS :thm -> thm list
-  val DISCH     :cterm -> thm -> thm
-  val UNDISCH   :thm  -> thm
-  val INST_TYPE :(typ*typ)list -> thm -> thm
-  val SPEC      :cterm -> thm -> thm
-  val ISPEC     :cterm -> thm -> thm
-  val ISPECL    :cterm list -> thm -> thm
-  val GEN       :cterm -> thm -> thm
-  val GENL      :cterm list -> thm -> thm
-  val LIST_CONJ :thm list -> thm
-
-  val SYM : thm -> thm
-  val DISCH_ALL : thm -> thm
-  val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
-  val SPEC_ALL  : thm -> thm
-  val GEN_ALL   : thm -> thm
-  val IMP_TRANS : thm -> thm -> thm
-  val PROVE_HYP : thm -> thm -> thm
-
-  val CHOOSE : cterm * thm -> thm -> thm
-  val EXISTS : cterm * cterm -> thm -> thm
-  val EXISTL : cterm list -> thm -> thm
-  val IT_EXISTS : (cterm*cterm) list -> thm -> thm
-
-  val EVEN_ORS : thm list -> thm list
-  val DISJ_CASESL : thm -> thm list -> thm
-
-  val list_beta_conv : cterm -> cterm list -> thm
-  val SUBS : thm list -> thm -> thm
-  val simpl_conv : simpset -> thm list -> cterm -> thm
-
-  val rbeta : thm -> thm
-(* For debugging my isabelle solver in the conditional rewriter *)
-  val term_ref : term list ref
-  val thm_ref : thm list ref
-  val mss_ref : meta_simpset list ref
-  val tracing : bool ref
-  val CONTEXT_REWRITE_RULE : term * term list * thm * thm list 
-                             -> thm -> thm * term list
-  val RIGHT_ASSOC : thm -> thm 
-
-  val prove : cterm * tactic -> thm
-end;
diff -r b4a170f7d658 -r 9a39eabfa17b TFL/tfl.sig
--- a/TFL/tfl.sig	Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(*  Title:      TFL/tfl
-    ID:         $Id$
-    Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-Main module
-*)
-
-signature TFL_sig =
-sig
-
-   val trace : bool ref
-
-   val default_simps : thm list      (*simprules used for deriving rules...*)
-
-   val Add_recdef_congs: thm list -> unit
-   val Del_recdef_congs: thm list -> unit
-   val init: theory -> theory
-   val print_recdef_congs: theory -> unit
-   val congs : theory -> thm list -> thm list  (*fn to make congruence rules*)
-
-   type pattern
-
-   val mk_functional : theory -> term list
-                       -> {functional:term,
-                           pats: pattern list}
-
-   val wfrec_definition0 : theory -> string -> term -> term -> theory * thm
-
-   val post_definition : thm list -> theory * (thm * pattern list)
-				  -> {theory : theory,
-				     rules  : thm,
-                                      rows  : int list,
-				       TCs  : term list list,
-			     full_pats_TCs  : (term * term list) list}
-
-   val wfrec_eqns : theory -> xstring
-	             -> thm list (* congruence rules *)
-                     -> term list
-                     -> {WFR : term,  SV : term list,
-                         proto_def : term,
-                         extracta :(thm * term list) list,
-                         pats  : pattern list}
-
-   val lazyR_def : theory -> xstring
-	           -> thm list (* congruence rules *)
-                   -> term list
-                   -> {theory : theory,
-                       rules : thm,
-                       R : term, 
-                       SV : term list,
-                       full_pats_TCs : (term * term list) list, 
-                       patterns : pattern list}
-
-   val mk_induction : theory 
-                       -> {fconst:term,
-                           R : term,
-                           SV : term list,
-                           pat_TCs_list : (term * term list) list}
-                       -> thm
-
-   val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
-                     -> theory 
-                      -> {rules:thm, induction:thm, TCs:term list list}
-                       -> {rules:thm, induction:thm, nested_tcs:thm list}
-end;
diff -r b4a170f7d658 -r 9a39eabfa17b TFL/thms.sig
--- a/TFL/thms.sig	Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      TFL/thms
-    ID:         $Id$
-    Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-*)
-
-signature Thms_sig =
-sig
-   val WF_INDUCTION_THM:thm
-   val WFREC_COROLLARY :thm
-   val CUT_DEF         :thm
-   val SELECT_AX       :thm
-   
-   val LET_CONG  :thm
-
-   val eqT       :thm
-   val rev_eq_mp :thm
-   val simp_thm  :thm
-end;
diff -r b4a170f7d658 -r 9a39eabfa17b TFL/thry.sig
--- a/TFL/thry.sig	Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      TFL/thry
-    ID:         $Id$
-    Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-*)
-
-signature Thry_sig =
-sig
-  val match_term : theory -> term -> term 
-                    -> (term*term)list * (typ*typ)list
-
-  val match_type : theory -> typ -> typ -> (typ*typ)list
-
-  val typecheck : theory -> term -> cterm
-
-  (* Datatype facts of various flavours *)
-  val match_info: theory -> string -> {constructors:term list,
-                                     case_const:term} option
-
-  val induct_info: theory -> string -> {constructors:term list,
-                                      nchotomy:thm} option
-
-  val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
-
-end;
-
-
diff -r b4a170f7d658 -r 9a39eabfa17b TFL/usyntax.sig
--- a/TFL/usyntax.sig	Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(*  Title:      TFL/usyntax
-    ID:         $Id$
-    Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-Emulation of HOL's abstract syntax functions
-*)
-
-signature USyntax_sig =
-sig
-  structure Utils : Utils_sig
-
-  datatype lambda = VAR   of {Name : string, Ty : typ}
-                  | CONST of {Name : string, Ty : typ}
-                  | COMB  of {Rator: term, Rand : term}
-                  | LAMB  of {Bvar : term, Body : term}
-
-  val alpha : typ
-
-  (* Types *)
-  val type_vars  : typ -> typ list
-  val type_varsl : typ list -> typ list
-  val mk_vartype : string -> typ
-  val is_vartype : typ -> bool
-  val strip_prod_type : typ -> typ list
-
-  (* Terms *)
-  val free_vars_lr : term -> term list
-  val type_vars_in_term : term -> typ list
-  val dest_term  : term -> lambda
-  
-  (* Prelogic *)
-  val inst      : (typ*typ) list -> term -> term
-
-  (* Construction routines *)
-  val mk_abs    :{Bvar  : term, Body : term} -> term
-
-  val mk_imp    :{ant : term, conseq :  term} -> term
-  val mk_select :{Bvar : term, Body : term} -> term
-  val mk_forall :{Bvar : term, Body : term} -> term
-  val mk_exists :{Bvar : term, Body : term} -> term
-  val mk_conj   :{conj1 : term, conj2 : term} -> term
-  val mk_disj   :{disj1 : term, disj2 : term} -> term
-  val mk_pabs   :{varstruct : term, body : term} -> term
-
-  (* Destruction routines *)
-  val dest_const: term -> {Name : string, Ty : typ}
-  val dest_comb : term -> {Rator : term, Rand : term}
-  val dest_abs  : term -> {Bvar : term, Body : term}
-  val dest_eq     : term -> {lhs : term, rhs : term}
-  val dest_imp    : term -> {ant : term, conseq : term}
-  val dest_forall : term -> {Bvar : term, Body : term}
-  val dest_exists : term -> {Bvar : term, Body : term}
-  val dest_neg    : term -> term
-  val dest_conj   : term -> {conj1 : term, conj2 : term}
-  val dest_disj   : term -> {disj1 : term, disj2 : term}
-  val dest_pair   : term -> {fst : term, snd : term}
-  val dest_pabs   : term -> {varstruct : term, body : term}
-
-  val lhs   : term -> term
-  val rhs   : term -> term
-  val rand  : term -> term
-
-  (* Query routines *)
-  val is_imp    : term -> bool
-  val is_forall : term -> bool 
-  val is_exists : term -> bool 
-  val is_neg    : term -> bool
-  val is_conj   : term -> bool
-  val is_disj   : term -> bool
-  val is_pair   : term -> bool
-  val is_pabs   : term -> bool
-
-  (* Construction of a term from a list of Preterms *)
-  val list_mk_abs    : (term list * term) -> term
-  val list_mk_imp    : (term list * term) -> term
-  val list_mk_forall : (term list * term) -> term
-  val list_mk_conj   : term list -> term
-
-  (* Destructing a term to a list of Preterms *)
-  val strip_comb     : term -> (term * term list)
-  val strip_abs      : term -> (term list * term)
-  val strip_imp      : term -> (term list * term)
-  val strip_forall   : term -> (term list * term)
-  val strip_exists   : term -> (term list * term)
-  val strip_disj     : term -> term list
-
-  (* Miscellaneous *)
-  val mk_vstruct : typ -> term list -> term
-  val gen_all    : term -> term
-  val find_term  : (term -> bool) -> term -> term option
-  val dest_relation : term -> term * term * term
-  val is_WFR : term -> bool
-  val ARB : typ -> term
-end;
diff -r b4a170f7d658 -r 9a39eabfa17b TFL/utils.sig
--- a/TFL/utils.sig	Tue Sep 05 18:51:49 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      TFL/utils
-    ID:         $Id$
-    Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
-
-Basic utilities
-*)
-
-signature Utils_sig =
-sig
-  exception ERR of {module:string,func:string, mesg:string}
-
-  val can   : ('a -> 'b) -> 'a -> bool
-  val holds : ('a -> bool) -> 'a -> bool
-  val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
-
-  val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
-  val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
-  val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a
-  val itlist2 :('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
-  val pluck : ('a -> bool) -> 'a list -> 'a * 'a list
-  val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
-  val take  : ('a -> 'b) -> int * 'a list -> 'b list
-  val sort  : ('a -> 'a -> bool) -> 'a list -> 'a list
-
-end;
-