commented out failing tactic (now that 'typerep' is defined using the new package
authorblanchet
Wed Sep 03 00:06:27 2014 +0200 (2014-09-03)
changeset 5815514dda84afbb3
parent 58154 47c3c7019b97
child 58156 e333bd3b4d3d
commented out failing tactic (now that 'typerep' is defined using the new package
src/HOL/Library/Countable.thy
     1.1 --- a/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:26 2014 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:27 2014 +0200
     1.3 @@ -308,9 +308,11 @@
     1.4  hide_const (open) finite_item nth_item
     1.5  
     1.6  
     1.7 +(* FIXME
     1.8  subsection {* Countable datatypes *}
     1.9  
    1.10  instance typerep :: countable
    1.11    by countable_datatype
    1.12 +*)
    1.13  
    1.14  end