# HG changeset patch
# User oheimb
# Date 982691250 -3600
# Node ID 2c90a6167b0b1590e6de5691c9dfd26aed49cd02
# Parent  eca861fd1eb5c00691a542106e108fa92546779c
added same_fstI

diff -r eca861fd1eb5 -r 2c90a6167b0b src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Tue Feb 20 18:47:29 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.ML	Tue Feb 20 18:47:30 2001 +0100
@@ -205,6 +205,10 @@
  * Wellfoundedness of same_fst
  *---------------------------------------------------------------------------*)
 
+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";
+
 val prems = goalw thy [same_fst_def]
   "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
 by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);