--- a/src/HOL/Codatatype/BNF_Util.thy Tue Sep 11 17:09:39 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Util.thy Tue Sep 11 17:14:49 2012 +0200
@@ -13,6 +13,8 @@
"../Ordinals_and_Cardinals/Cardinal_Arithmetic"
"~~/src/HOL/Library/Prefix_Order"
Equiv_Relations_More
+uses
+ ("Tools/bnf_util.ML")
begin
lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
@@ -851,4 +853,7 @@
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
by simp
+ML_file "Tools/bnf_util.ML"
+ML_file "Tools/bnf_tactics.ML"
+
end