src/HOL/Wellfounded.thy
changeset 35216 7641e8d831d2
parent 33217 ab979f6e99f4
child 35719 99b6152aedf5
     1.1 --- a/src/HOL/Wellfounded.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Wellfounded.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -489,7 +489,7 @@
     1.4    by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
     1.5  
     1.6  lemma trans_less_than [iff]: "trans less_than"
     1.7 -  by (simp add: less_than_def trans_trancl)
     1.8 +  by (simp add: less_than_def)
     1.9  
    1.10  lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
    1.11    by (simp add: less_than_def less_eq)