reintroduced old setup for size of basic types
authorblanchet
Fri Sep 19 13:27:04 2014 +0200 (2014-09-19)
changeset 58391fe0fc8aee49a
parent 58390 b74d8470b98e
child 58392 00f5b1efc741
reintroduced old setup for size of basic types
src/HOL/Basic_BNF_Least_Fixpoints.thy
     1.1 --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
     1.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
     1.3 @@ -57,6 +57,14 @@
     1.4  
     1.5  ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
     1.6  
     1.7 +lemma size_bool[code]: "size (b\<Colon>bool) = 0"
     1.8 +  by (cases b) auto
     1.9 +
    1.10 +declare prod.size[no_atp]
    1.11 +
    1.12 +lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    1.13 +  by (induct n) simp_all
    1.14 +
    1.15  hide_const (open) xtor ctor_rec
    1.16  
    1.17  hide_fact (open)