changeset 49309 | f20b24214ac2 |
parent 49286 | dde4967c9233 |
child 49312 | c874ff5658dc |
--- a/src/HOL/Codatatype/BNF_Wrap.thy Wed Sep 12 05:03:18 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Wrap.thy Wed Sep 12 05:21:47 2012 +0200 @@ -12,9 +12,9 @@ keywords "wrap_data" :: thy_goal and "no_dests" -uses - "Tools/bnf_wrap_tactics.ML" - "Tools/bnf_wrap.ML" begin +ML_file "Tools/bnf_wrap_tactics.ML" +ML_file "Tools/bnf_wrap.ML" + end