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