--- a/TFL/rules.sig Tue May 27 13:03:41 1997 +0200
+++ b/TFL/rules.sig Tue May 27 13:22:30 1997 +0200
@@ -9,8 +9,6 @@
signature Rules_sig =
sig
(* structure USyntax : USyntax_sig *)
- type 'a binding
-
val dest_thm : thm -> term list * term
(* Inference rules *)
@@ -23,7 +21,7 @@
val CONJUNCTS :thm -> thm list
val DISCH :cterm -> thm -> thm
val UNDISCH :thm -> thm
- val INST_TYPE :typ binding list -> 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
@@ -42,7 +40,7 @@
val CHOOSE : cterm * thm -> thm -> thm
val EXISTS : cterm * cterm -> thm -> thm
val EXISTL : cterm list -> thm -> thm
- val IT_EXISTS : cterm binding 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