--- a/Trancl.ML	Fri Nov 25 13:34:33 1994 +0100
+++ b/Trancl.ML	Fri Nov 25 13:35:32 1994 +0100
@@ -37,6 +37,10 @@
 by (eresolve_tac prems 1);
 qed "idE";
 
+goalw Trancl.thy [id_def] "<a,b>:id = (a=b)";
+by(fast_tac prod_cs 1);
+qed "pair_in_id_conv";
+
 (** Composition of two relations **)
 
 val prems = goalw Trancl.thy [comp_def]
@@ -230,3 +234,4 @@
 by (fast_tac (comp_cs addSDs [trancl_subset_Sigma_lemma]) 1);
 qed "trancl_subset_Sigma";
 
+val prod_ss = prod_ss addsimps [pair_in_id_conv];