| changeset 62335 | e85c42f4f30a |
| parent 62321 | 1abe81758619 |
| child 62863 | e0b894bba6ff |
--- a/src/HOL/Basic_BNF_LFPs.thy Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Basic_BNF_LFPs.thy Wed Feb 17 17:08:36 2016 +0100 @@ -97,7 +97,7 @@ ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" -lemma size_bool[code]: "size (b::bool) = 0" +lemma size_bool[code]: "size (b :: bool) = 0" by (cases b) auto declare prod.size[no_atp]