author | mengj |
Sat, 30 Sep 2006 14:29:52 +0200 | |
changeset 20788 | d51711512d07 |
parent 20787 | 406d990006af |
child 20789 | e279499c4f80 |
--- a/src/HOL/Reconstruction.thy Fri Sep 29 22:47:51 2006 +0200 +++ b/src/HOL/Reconstruction.thy Sat Sep 30 14:29:52 2006 +0200 @@ -54,8 +54,8 @@ lemma equal_imp_fequal: "X=Y ==> fequal X Y" by (simp add: fequal_def) +use "Tools/res_axioms.ML" use "Tools/res_hol_clause.ML" -use "Tools/res_axioms.ML" use "Tools/res_atp.ML" use "Tools/reconstruction.ML"