src/HOL/IsaMakefile
changeset 32618 42865636d006
parent 32558 e6e1fc2e73cb
child 32621 a073cb249a06
     1.1 --- a/src/HOL/IsaMakefile	Fri Sep 18 14:40:24 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 18 18:13:19 2009 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4    HOL-Prolog \
     1.5    HOL-SET-Protocol \
     1.6    HOL-SizeChange \
     1.7 +  HOL-SMT \
     1.8    HOL-Statespace \
     1.9    HOL-Subst \
    1.10        TLA-Buffer \
    1.11 @@ -1134,6 +1135,19 @@
    1.12  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    1.13  
    1.14  
    1.15 +## HOL-SMT
    1.16 +
    1.17 +HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz
    1.18 +
    1.19 +$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Definitions.thy SMT/SMT.thy \
    1.20 +  SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
    1.21 +  SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
    1.22 +  SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
    1.23 +  SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
    1.24 +  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML SMT/Tools/z3_model.ML
    1.25 +	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
    1.26 +
    1.27 +
    1.28  ## clean
    1.29  
    1.30  clean:
    1.31 @@ -1156,4 +1170,4 @@
    1.32  		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
    1.33  		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
    1.34  		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz            \
    1.35 -                $(LOG)/HOL-Mirabelle.gz
    1.36 +                $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz