| changeset 59819 | dbec7f33093d |
| parent 59141 | 9a5c2e9b001e |
| child 61076 | bdc1e2f0a86a |
--- a/src/HOL/Basic_BNF_LFPs.thy Thu Mar 26 16:42:42 2015 +0100 +++ b/src/HOL/Basic_BNF_LFPs.thy Thu Mar 26 17:10:24 2015 +0100 @@ -99,8 +99,7 @@ declare prod.size[no_atp] -lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" - by (induct n) simp_all +lemmas size_nat = size_nat_def hide_const (open) xtor ctor_rec