src/HOL/Wellfounded_Relations.thy
changeset 15348 0a60f15c2d7a
parent 15346 ac272926fb77
child 15352 cba05842bd7a
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Tue Nov 30 18:25:55 2004 +0100
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Dec 01 04:11:15 2004 +0100
     1.3 @@ -133,7 +133,7 @@
     1.4  by (blast intro: finite_acyclic_wf wf_acyclic)
     1.5  
     1.6  
     1.7 -subsubsection{*Wellfoundedness of same_fst*}
     1.8 +subsubsection{*Wellfoundedness of same\_fst*}
     1.9  
    1.10  lemma same_fstI [intro!]:
    1.11       "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"