# HG changeset patch # User wenzelm # Date 1144922454 -7200 # Node ID 3a9d25bdd7f4b65d9753e2b54f23dcb9eb813afd # Parent 4198e7698f6abc8abba6c09006ef3d4b91c27aaa added conjunction.ML; diff -r 4198e7698f6a -r 3a9d25bdd7f4 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Apr 13 12:00:53 2006 +0200 +++ b/src/Pure/ROOT.ML Thu Apr 13 12:00:54 2006 +0200 @@ -50,6 +50,7 @@ use "tctical.ML"; use "search.ML"; use "meta_simplifier.ML"; +use "conjunction.ML"; use "goal.ML"; use "tactic.ML";