--- a/src/Pure/drule.ML Fri Sep 01 13:16:24 1995 +0200
+++ b/src/Pure/drule.ML Fri Sep 01 13:27:48 1995 +0200
@@ -26,6 +26,7 @@
val equal_abs_elim : cterm -> thm -> thm
val equal_abs_elim_list: cterm list -> thm -> thm
val eq_thm : thm * thm -> bool
+ val same_thm : thm * thm -> bool
val eq_thm_sg : thm * thm -> bool
val flexpair_abs_elim_list: cterm list -> thm -> thm
val forall_intr_list : cterm list -> thm -> thm
@@ -648,6 +649,18 @@
prop1 aconv prop2
end;
+(*equality of theorems using similarity of signatures,
+ i.e. the theorems belong to the same theory but not necessarily to the same
+ version of this theory*)
+fun same_thm (th1,th2) =
+ let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
+ and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
+ in Sign.same_sg (sg1,sg2) andalso
+ eq_set (shyps1, shyps2) andalso
+ aconvs(hyps1,hyps2) andalso
+ prop1 aconv prop2
+ end;
+
(*Do the two theorems have the same signature?*)
fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
--- a/src/Pure/sign.ML Fri Sep 01 13:16:24 1995 +0200
+++ b/src/Pure/sign.ML Fri Sep 01 13:27:48 1995 +0200
@@ -20,6 +20,7 @@
stamps: string ref list}
val subsig: sg * sg -> bool
val eq_sg: sg * sg -> bool
+ val same_sg: sg * sg -> bool
val is_draft: sg -> bool
val const_type: sg -> string -> typ option
val classes: sg -> class list
@@ -107,6 +108,12 @@
fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
+(* test if same theory names are contained in signatures' stamps,
+ i.e. if signatures belong to same theory but not necessarily to the same
+ version of it*)
+fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
+ eq_set (pairself (map (op !)) (s1, s2));
+
(* consts *)