# HG changeset patch # User paulson # Date 826911504 -3600 # Node ID 97a305db0c9e8979227dd64998fa69f696ec6ef8 # Parent a82618a900e5d5e08adae920b0fc92babae43e95 Updated for new file search.ML diff -r a82618a900e5 -r 97a305db0c9e src/Pure/Makefile --- a/src/Pure/Makefile Fri Mar 15 13:34:39 1996 +0100 +++ b/src/Pure/Makefile Fri Mar 15 18:38:24 1996 +0100 @@ -23,7 +23,8 @@ COMP = $(ISABELLECOMP) FILES = POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\ sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\ - net.ML drule.ML tctical.ML tactic.ML goals.ML axclass.ML install_pp.ML\ + net.ML drule.ML tctical.ML search.ML tactic.ML\ + goals.ML axclass.ML install_pp.ML\ NJ093.ML NJ1xx.ML ../Provers/simplifier.ML SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ diff -r a82618a900e5 -r 97a305db0c9e src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Mar 15 13:34:39 1996 +0100 +++ b/src/Pure/ROOT.ML Fri Mar 15 18:38:24 1996 +0100 @@ -37,6 +37,7 @@ use "thm.ML"; use "drule.ML"; use "tctical.ML"; +use "search.ML"; use "tactic.ML"; use "goals.ML"; use "axclass.ML";