changeset 55062 | 6d3fad6f01c9 |
parent 55059 | ef2e0fb783c6 |
child 55066 | 4e5ddf3162ac |
--- a/src/HOL/BNF_Def.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Def.thy Mon Jan 20 18:24:56 2014 +0100 @@ -157,7 +157,7 @@ lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v" by clarsimp -ML_file "Tools/bnf_def_tactics.ML" -ML_file "Tools/bnf_def.ML" +ML_file "Tools/BNF/bnf_def_tactics.ML" +ML_file "Tools/BNF/bnf_def.ML" end