# HG changeset patch # User blanchet # Date 1409695587 -7200 # Node ID 14dda84afbb30615fff33fc88b98039fe23d613a # Parent 47c3c7019b976dd122f5b0e846950803f85ced3b commented out failing tactic (now that 'typerep' is defined using the new package diff -r 47c3c7019b97 -r 14dda84afbb3 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Wed Sep 03 00:06:26 2014 +0200 +++ b/src/HOL/Library/Countable.thy Wed Sep 03 00:06:27 2014 +0200 @@ -308,9 +308,11 @@ hide_const (open) finite_item nth_item +(* FIXME subsection {* Countable datatypes *} instance typerep :: countable by countable_datatype +*) end