Trancl.ML

 \    |] ==>  P";  
 by (rtac (major RS CollectE) 1);
 by (etac exE 1);
 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]
     "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";

 goalw Trancl.thy [trancl_def]
     "!!r. r <= Sigma(A,%x.A) ==> trancl(r) <= Sigma(A,%x.A)";
 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];