author | blanchet |
Wed, 03 Sep 2014 22:47:05 +0200 | |
changeset 58167 | 08052d9f8050 |
parent 58166 | 86a374caeb82 |
child 58168 | 6b6c41aa780b |
--- a/src/HOL/BNF_Examples/Misc_Datatype.thy Wed Sep 03 22:47:05 2014 +0200 +++ b/src/HOL/BNF_Examples/Misc_Datatype.thy Wed Sep 03 22:47:05 2014 +0200 @@ -207,11 +207,8 @@ instance tree' and branch :: (countable) countable by countable_datatype -(* FIXME: - instance bin_rose_tree :: (countable) countable by countable_datatype -*) instance exp and trm and factor :: (countable, countable) countable by countable_datatype