# HG changeset patch
# User blanchet
# Date 1411126024 -7200
# Node ID fe0fc8aee49aecf9d70f5ed5bc2c1e7809da69f3
# Parent  b74d8470b98e0b0c76fcaaeab2fe00c68da748ac
reintroduced old setup for size of basic types

diff -r b74d8470b98e -r fe0fc8aee49a src/HOL/Basic_BNF_Least_Fixpoints.thy
--- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
@@ -57,6 +57,14 @@
 
 ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
 
+lemma size_bool[code]: "size (b\<Colon>bool) = 0"
+  by (cases b) auto
+
+declare prod.size[no_atp]
+
+lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
+  by (induct n) simp_all
+
 hide_const (open) xtor ctor_rec
 
 hide_fact (open)