--- a/src/Pure/thm.ML Tue May 31 11:53:25 2005 +0200
+++ b/src/Pure/thm.ML Tue May 31 11:53:26 2005 +0200
@@ -48,6 +48,7 @@
exception THM of string * int * thm list
type 'a attribute (* = 'a * thm -> 'a * thm *)
val eq_thm : thm * thm -> bool
+ val eq_thms : thm list * thm list -> bool
val sign_of_thm : thm -> Sign.sg
val prop_of : thm -> term
val proof_of : thm -> Proofterm.proof
@@ -342,6 +343,8 @@
prop1 aconv prop2
end;
+val eq_thms = Library.equal_lists eq_thm;
+
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
fun prop_of (Thm {prop, ...}) = prop;
fun proof_of (Thm {der = (_, proof), ...}) = proof;