# HG changeset patch # User blanchet # Date 1409777225 -7200 # Node ID 68a2cf857df1f65142839a8922f2c585c589ce41 # Parent 6b6c41aa780b958c7f929dafeb6978ca7db9d133 reintroduced more examples diff -r 6b6c41aa780b -r 68a2cf857df1 src/HOL/BNF_Examples/Misc_Datatype.thy --- 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 @@ -237,26 +237,26 @@ instance kk1 and kk2 :: countable by countable_datatype -(* FIXME: - instance t1 and t2 and t3 :: countable by countable_datatype instance t1' and t2' and t3' :: countable by countable_datatype +(* FIXME: + instance k1 and k2 and k3 and k4 :: countable by countable_datatype instance tt1 and tt2 and tt3 and tt4 :: countable by countable_datatype +*) instance d1 :: countable by countable_datatype instance d1' :: countable by countable_datatype -*) instance d2 :: countable by countable_datatype