src/HOL/Library/Countable.thy
changeset 62691 9bfcbab7cd99
parent 62087 44841d07ef1d
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Library/Countable.thy	Tue Mar 22 08:00:33 2016 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4  
     1.5  subsection \<open>Automatically proving countability of datatypes\<close>
     1.6  
     1.7 -ML_file "bnf_lfp_countable.ML"
     1.8 +ML_file "../Tools/BNF/bnf_lfp_countable.ML"
     1.9  
    1.10  ML \<open>
    1.11  fun countable_datatype_tac ctxt st =