| changeset 46635 | cde737f9c911 |
| parent 46356 | 48fcca8965f4 |
| child 46638 | fc315796794e |
--- a/src/HOL/Wellfounded.thy Thu Feb 23 21:16:54 2012 +0100 +++ b/src/HOL/Wellfounded.thy Thu Feb 23 21:25:59 2012 +0100 @@ -858,10 +858,4 @@ declare "prod.size" [no_atp] -lemma [code]: - "size (P :: 'a Predicate.pred) = 0" by (cases P) simp - -lemma [code]: - "pred_size f P = 0" by (cases P) simp - end