1.1 --- a/src/HOL/Wellfounded_Relations.ML	Tue Feb 20 18:47:29 2001 +0100
     1.2 +++ b/src/HOL/Wellfounded_Relations.ML	Tue Feb 20 18:47:30 2001 +0100
     1.3 @@ -205,6 +205,10 @@
     1.4   * Wellfoundedness of same_fst
     1.5   *---------------------------------------------------------------------------*)
     1.6  
     1.7 +Goalw[same_fst_def] "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R";
     1.8 +by (Asm_simp_tac 1);
     1.9 +qed "same_fstI";
    1.10 +
    1.11  val prems = goalw thy [same_fst_def]
    1.12    "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
    1.13  by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);