| changeset 11340 | 34a9a9126c49 |
| parent 11167 | 2c90a6167b0b |
| child 11454 | 7514e5e21cb8 |
--- 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)";