src/HOL/BNF_LFP.thy
changeset 55062 6d3fad6f01c9
parent 55059 ef2e0fb783c6
child 55066 4e5ddf3162ac
--- a/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -234,10 +234,10 @@
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   unfolding vimage2p_def by auto
 
-ML_file "Tools/bnf_lfp_rec_sugar.ML"
-ML_file "Tools/bnf_lfp_util.ML"
-ML_file "Tools/bnf_lfp_tactics.ML"
-ML_file "Tools/bnf_lfp.ML"
-ML_file "Tools/bnf_lfp_compat.ML"
+ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
+ML_file "Tools/BNF/bnf_lfp_util.ML"
+ML_file "Tools/BNF/bnf_lfp_tactics.ML"
+ML_file "Tools/BNF/bnf_lfp.ML"
+ML_file "Tools/BNF/bnf_lfp_compat.ML"
 
 end