# HG changeset patch
# User nipkow
# Date 785766932 -3600
# Node ID d8a5435732cf0941336f342a6e53adecb36ec609
# Parent  74ce9774c9234bf8b038d0292391cce7fd120563
added id_in_pair_conv

diff -r 74ce9774c923 -r d8a5435732cf Trancl.ML
--- 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];