# HG changeset patch
# User wenzelm
# Date 1117533206 -7200
# Node ID c66545fe72bf9110a9e6671954e5d0082f4698d6
# Parent  89ea482e1649fd0c2d2464193ad8996383c8bc7d
added eq_thms;

diff -r 89ea482e1649 -r c66545fe72bf src/Pure/thm.ML
--- 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;