| changeset 30430 | 42ea5d85edcc |
| parent 29609 | a010aab5bed0 |
| child 30988 | b53800e3ee47 |
--- a/src/HOL/Wellfounded.thy Wed Mar 11 08:45:47 2009 +0100 +++ b/src/HOL/Wellfounded.thy Wed Mar 11 08:45:47 2009 +0100 @@ -960,4 +960,10 @@ declare "prod.size" [noatp] +lemma [code]: + "size (P :: 'a Predicate.pred) = 0" by (cases P) simp + +lemma [code]: + "pred_size f P = 0" by (cases P) simp + end