src/HOL/Wellfounded_Relations.thy
changeset 19404 9bf2cdc9e8e8
parent 18277 6c2b039b4847
child 19623 12e6cc4382ae
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Mon Apr 10 14:37:23 2006 +0200
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Mon Apr 10 16:00:34 2006 +0200
     1.3 @@ -116,13 +116,11 @@
     1.4  apply (drule spec, erule mp, blast) 
     1.5  done
     1.6  
     1.7 -
     1.8  text{*Transitivity of WF combinators.*}
     1.9  lemma trans_lex_prod [intro!]: 
    1.10      "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
    1.11  by (unfold trans_def lex_prod_def, blast) 
    1.12  
    1.13 -
    1.14  subsubsection{*Wellfoundedness of proper subset on finite sets.*}
    1.15  lemma wf_finite_psubset: "wf(finite_psubset)"
    1.16  apply (unfold finite_psubset_def)