changeset 55538 | 6a5986170c1d |
parent 55463 | 942c2153b5b4 |
child 55542 | 4394bb0b522b |
--- a/src/HOL/BNF_GFP.thy Mon Feb 17 14:59:09 2014 +0100 +++ b/src/HOL/BNF_GFP.thy Mon Feb 17 18:18:27 2014 +0100 @@ -349,10 +349,10 @@ thus "univ f X \<in> B" using x PRES by simp qed -ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML" -ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML" ML_file "Tools/BNF/bnf_gfp_util.ML" ML_file "Tools/BNF/bnf_gfp_tactics.ML" ML_file "Tools/BNF/bnf_gfp.ML" +ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML" +ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML" end