fixed presentation
authorpaulson
Wed Dec 01 12:53:49 2004 +0100 (2004-12-01)
changeset 15352cba05842bd7a
parent 15351 bdcd0f321df0
child 15353 b53b89d3bf03
fixed presentation
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Wed Dec 01 10:14:10 2004 +0100
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Dec 01 12:53:49 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 @{term 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"