changeset 1008 | fa11e1e28bd3 |
parent 393 | 02b27671b899 |
child 1296 | ae31bb7774a7 |
--- a/src/FOLP/ROOT.ML Thu Apr 06 11:09:15 1995 +0200 +++ b/src/FOLP/ROOT.ML Thu Apr 06 11:12:35 1995 +0200 @@ -18,10 +18,9 @@ use_thy "IFOLP"; use_thy "FOLP"; -use "../Provers/hypsubst.ML"; +use "hypsubst.ML"; use "classical.ML"; (* Patched 'cos matching won't instantiate proof *) use "simp.ML"; (* Patched 'cos matching won't instantiate proof *) -use "../Provers/ind.ML"; (*** Applying HypsubstFun to generate hyp_subst_tac ***)