# HG changeset patch
# User oheimb
# Date 991320616 -7200
# Node ID 34a9a9126c49baad1c1781452a1075a4941d221d
# Parent  3fb4d00b294acccc7e6debad51fca0807e9baafb
added same_fstI as safe intro rule

diff -r 3fb4d00b294a -r 34a9a9126c49 src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Thu May 31 16:50:15 2001 +0200
+++ b/src/HOL/Wellfounded_Relations.ML	Thu May 31 16:50:16 2001 +0200
@@ -208,6 +208,7 @@
 Goalw[same_fst_def] "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R";
 by (Asm_simp_tac 1);
 qed "same_fstI";
+AddSIs[same_fstI];
 
 val prems = goalw thy [same_fst_def]
   "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";