# HG changeset patch
# User boehmes
# Date 1253533356 -7200
# Node ID a45e8ec2b51ee24ae014da629839deb059a8ed9b
# Parent  f270520df7dee22297115fb9be109c2b4ee199a5
deleted unused file

diff -r f270520df7de -r a45e8ec2b51e src/HOL/SMT/IsaMakefile
--- a/src/HOL/SMT/IsaMakefile	Mon Sep 21 12:23:05 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-## targets
-
-default: HOL-SMT
-images: HOL-SMT
-test: 
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISATOOL) usedir -v true 
-
-
-## HOL-SMT
-
-HOL-SMT: $(OUT)/HOL-SMT
-
-$(OUT)/HOL-SMT: $(OUT)/HOL-Word ROOT.ML SMT_Definitions.thy SMT.thy \
-  Tools/cancel_conj_disj.ML Tools/smt_normalize.ML Tools/smt_monomorph.ML \
-  Tools/smt_translate.ML Tools/smt_builtin.ML Tools/smtlib_interface.ML \
-  Tools/smt_solver.ML Tools/cvc3_solver.ML Tools/yices_solver.ML \
-  Tools/z3_interface.ML Tools/z3_solver.ML Tools/z3_model.ML \
-  Tools/z3_proof.ML Tools/z3_proof_rules.ML Tools/z3_proof_terms.ML
-	@$(USEDIR) -b HOL-Word HOL-SMT
-
-$(OUT)/HOL-Word:
-	@$(ISATOOL) make HOL-Word -C $(SRC)/HOL
-
-
-## clean
-
-clean:
-	@rm -f $(OUT)/HOL-SMT