# HG changeset patch # User wenzelm # Date 884177622 -3600 # Node ID 74c01296e8185a5e0a6c20230fe92bdc3f48e12e # Parent fad9b7479dbe4d508f731eb554e774642084380c improved targets; fixed dependencies on parent logics; diff -r fad9b7479dbe -r 74c01296e818 src/CCL/IsaMakefile --- a/src/CCL/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/CCL/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,33 +4,46 @@ # IsaMakefile for CCL # +## targets + +default: CCL +images: CCL +test: CCL-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \ - Gfp.thy Gfp.ML Lfp.thy Lfp.ML + +## CCL + +CCL: FOL $(OUT)/CCL -CCL_FILES = CCL.thy CCL.ML Term.thy Term.ML Type.thy Type.ML \ - coinduction.ML Hered.thy Hered.ML Trancl.thy Trancl.ML \ - Wfd.thy Wfd.ML genrec.ML typecheck.ML eval.ML Fix.thy Fix.ML +FOL: + @cd $(SRC)/FOL; $(ISATOOL) make FOL -EX_FILES = ex/ROOT.ML ex/Flag.ML ex/Flag.thy ex/List.ML ex/List.thy \ - ex/Nat.ML ex/Nat.thy ex/Stream.ML ex/Stream.thy - - -$(OUT)/CCL: $(OUT)/FOL $(SET_FILES) $(CCL_FILES) +$(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \ + Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \ + Term.thy Trancl.ML Trancl.thy Type.ML Type.thy Wfd.ML Wfd.thy \ + coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \ + typecheck.ML @$(ISATOOL) usedir -b $(OUT)/FOL CCL -$(OUT)/FOL: - @cd ../FOL; $(ISATOOL) make + +## CCL-ex -$(LOG)/CCL-ex.gz: ex/ROOT.ML $(OUT)/CCL $(EX_FILES) +CCL-ex: CCL $(LOG)/CCL-ex.gz + +$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.ML ex/Flag.thy ex/List.ML \ + ex/List.thy ex/Nat.ML ex/Nat.thy ex/ROOT.ML ex/Stream.ML ex/Stream.thy @$(ISATOOL) usedir $(OUT)/CCL ex -test: $(OUT)/CCL $(LOG)/CCL-ex.gz + +## clean clean: - @rm -f $(OUT)/CCL $(LOG)/CCL-ex.gz - - -.PRECIOUS: $(OUT)/FOL $(OUT)/CCL + @rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz diff -r fad9b7479dbe -r 74c01296e818 src/CTT/IsaMakefile --- a/src/CTT/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/CTT/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,27 +4,43 @@ # IsaMakefile for CTT # +## targets + +default: CTT +images: CTT +test: CTT-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ - Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML + +## CTT + +CTT: Pure $(OUT)/CTT -EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML +Pure: + @cd $(SRC)/Pure; $(ISATOOL) make Pure -$(OUT)/CTT: $(OUT)/Pure $(FILES) +$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \ + Bool.ML Bool.thy CTT.ML CTT.thy ROOT.ML rew.ML @$(ISATOOL) usedir -b $(OUT)/Pure CTT -$(OUT)/Pure: - @cd ../Pure; $(ISATOOL) make + +## CTT-ex -$(LOG)/CTT-ex.gz: ex/ROOT.ML $(OUT)/CTT $(EX_FILES) +CTT-ex: CTT $(LOG)/CTT-ex.gz + +$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/elim.ML ex/equal.ML \ + ex/synth.ML ex/typechk.ML @$(ISATOOL) usedir $(OUT)/CTT ex -test: $(OUT)/CTT $(LOG)/CTT-ex.gz + +## clean clean: - @rm -f $(OUT)/CTT $(LOG)/CTT-ex.gz - - -.PRECIOUS: $(OUT)/Pure $(OUT)/CTT + @rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz diff -r fad9b7479dbe -r 74c01296e818 src/Cube/IsaMakefile --- a/src/Cube/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/Cube/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,24 +4,41 @@ # IsaMakefile for Cube # +## targets + +default: Cube +images: Cube +test: Cube-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -FILES = ROOT.ML Cube.thy Cube.ML + +## Cube + +Cube: Pure $(OUT)/Cube -$(OUT)/Cube: $(OUT)/Pure $(FILES) +Pure: + @cd $(SRC)/Pure; $(ISATOOL) make Pure + +$(OUT)/Cube: $(OUT)/Pure Cube.ML Cube.thy ROOT.ML @$(ISATOOL) usedir -b $(OUT)/Pure Cube -$(OUT)/Pure: - @cd ../Pure; $(ISATOOL) make + +## Cube-ex -$(LOG)/Cube-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/Cube +Cube-ex: Cube $(LOG)/Cube-ex.gz + +$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ROOT.ML @$(ISATOOL) usedir $(OUT)/Cube ex -test: $(OUT)/Cube $(LOG)/Cube-ex.gz + +## clean clean: - @rm -f $(OUT)/Cube $(LOG)/Cube-ex.gz - - -.PRECIOUS: $(OUT)/Pure $(OUT)/Cube + @rm -f $(OUT)/Cube $(LOG)/Cube.gz $(LOG)/Cube-ex.gz diff -r fad9b7479dbe -r 74c01296e818 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/FOL/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,33 +4,48 @@ # IsaMakefile for FOL # +## targets + +default: FOL +images: FOL +test: FOL-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -PROVERS = hypsubst.ML classical.ML blast.ML \ - simplifier.ML splitter.ML ind.ML -FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \ - fologic.ML cladata.ML $(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%) +## FOL + +FOL: Pure $(OUT)/FOL -EX_NAMES = If List Nat Nat2 Prolog IffOracle -EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \ - ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) +Pure: + @cd $(SRC)/Pure; $(ISATOOL) make Pure - -$(OUT)/FOL: $(OUT)/Pure $(FILES) +$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ + $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \ + $(SRC)/Provers/ind.ML $(SRC)/Provers/simplifier.ML \ + $(SRC)/Provers/splitter.ML FOL.ML FOL.thy IFOL.ML IFOL.thy ROOT.ML \ + cladata.ML fologic.ML intprover.ML simpdata.ML @$(ISATOOL) usedir -b $(OUT)/Pure FOL -$(OUT)/Pure: - @cd ../Pure; $(ISATOOL) make + +## FOL-ex + +FOL-ex: FOL $(LOG)/FOL-ex.gz -$(LOG)/FOL-ex.gz: ex/ROOT.ML $(OUT)/FOL $(EX_FILES) +$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/If.ML ex/If.thy ex/IffOracle.ML \ + ex/IffOracle.thy ex/List.ML ex/List.thy ex/Nat.ML ex/Nat.thy \ + ex/Nat2.ML ex/Nat2.thy ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/cla.ML \ + ex/foundn.ML ex/int.ML ex/intro.ML ex/prop.ML ex/quant.ML @$(ISATOOL) usedir $(OUT)/FOL ex -test: $(OUT)/FOL $(LOG)/FOL-ex.gz + +## clean clean: - @rm -f $(OUT)/FOL $(LOG)/FOL-ex.gz - - -.PRECIOUS: $(OUT)/Pure $(OUT)/FOL + @rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz diff -r fad9b7479dbe -r 74c01296e818 src/FOLP/IsaMakefile --- a/src/FOLP/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/FOLP/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,29 +4,44 @@ # IsaMakefile for FOLP # +## targets + +default: FOLP +images: FOLP +test: FOLP-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \ - hypsubst.ML classical.ML simp.ML + +## FOLP + +FOLP: Pure $(OUT)/FOLP -EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML \ - ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy \ - ex/prop.ML ex/quant.ML +Pure: + @cd $(SRC)/Pure; $(ISATOOL) make Pure -$(OUT)/FOLP: $(OUT)/Pure $(FILES) +$(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \ + classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML @$(ISATOOL) usedir -b $(OUT)/Pure FOLP -$(OUT)/Pure: - @cd ../Pure; $(ISATOOL) make + +## FOLP-ex -$(LOG)/FOLP-ex.gz: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES) +FOLP-ex: FOLP $(LOG)/FOLP-ex.gz + +$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/foundn.ML \ + ex/If.ML ex/If.thy ex/int.ML ex/intro.ML ex/Nat.ML ex/Nat.thy \ + ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML @$(ISATOOL) usedir $(OUT)/FOLP ex -test: $(OUT)/FOLP $(LOG)/FOLP-ex.gz + +## clean clean: - @rm -f $(OUT)/FOLP $(LOG)/FOLP-ex.gz - - -.PRECIOUS: $(OUT)/Pure $(OUT)/FOLP + @rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz diff -r fad9b7479dbe -r 74c01296e818 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/HOL/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,267 +4,320 @@ # IsaMakefile for HOL # -#### Base system +## targets +default: HOL +images: HOL TLA +test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Integ \ + HOL-Auth HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \ + HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \ + HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \ - mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \ - Divides Power Sexp Univ List RelPow Option Map + +## HOL -PROVERS = hypsubst.ML classical.ML blast.ML \ - simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML +HOL: Pure $(OUT)/HOL + +Pure: + @cd $(SRC)/Pure; $(ISATOOL) make Pure -TFL = dcterm.sml post.sml rules.new.sml rules.sig \ - sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml \ - usyntax.sig usyntax.sml utils.sig utils.sml - -FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \ - ind_syntax.ML cladata.ML record.ML simpdata.ML arith_data.ML \ - typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \ - $(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \ - $(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%) - -$(OUT)/HOL: $(OUT)/Pure $(FILES) +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \ + $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \ + $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \ + $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ + $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \ + $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml \ + $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig \ + $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml \ + $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig \ + $(SRC)/TFL/utils.sml Arith.ML Arith.thy Divides.ML Divides.thy \ + Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \ + Inductive.ML Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML \ + Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy \ + Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML \ + RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \ + Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy WF.ML WF.thy \ + WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \ + datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \ + indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \ + record.ML simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML \ + typedef.ML @$(ISATOOL) usedir -b $(OUT)/Pure HOL -$(OUT)/Pure: - @cd ../Pure; $(ISATOOL) make + +## HOL-Subst + +HOL-Subst: HOL $(LOG)/HOL-Subst.gz + +$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.ML Subst/AList.thy \ + Subst/ROOT.ML Subst/Subst.ML Subst/Subst.thy Subst/UTerm.ML \ + Subst/UTerm.thy Subst/Unifier.ML Subst/Unifier.thy Subst/Unify.ML \ + Subst/Unify.thy + @$(ISATOOL) usedir $(OUT)/HOL Subst -#### Tests and examples +## HOL-Induct -## Inductive definitions: simple examples +HOL-Induct: HOL $(LOG)/HOL-Induct.gz -INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult Com Exp - -INDUCT_FILES = Induct/ROOT.ML \ - $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML) - -$(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES) +$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Acc.ML Induct/Acc.thy \ + Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \ + Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \ + Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \ + Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \ + Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/Simult.ML \ + Induct/Simult.thy Induct/Term.ML Induct/Term.thy @$(ISATOOL) usedir $(OUT)/HOL Induct -## IMP-semantics example +## HOL-IMP + +HOL-IMP: HOL $(LOG)/HOL-IMP.gz -IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC -IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) - -$(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES) +$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \ + IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \ + IMP/Natural.ML IMP/Natural.thy IMP/ROOT.ML IMP/Transition.ML \ + IMP/Transition.thy IMP/VC.ML IMP/VC.thy @$(ISATOOL) usedir $(OUT)/HOL IMP -## Hoare logic +## HOL-Hoare + +HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz -Hoare_NAMES = Hoare Arith2 Examples -Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \ - $(Hoare_NAMES:%=Hoare/%.ML) - -$(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES) +$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \ + Hoare/Examples.ML Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \ + Hoare/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL Hoare -## The integers in HOL +## HOL-Lex + +HOL-Lex: HOL $(LOG)/HOL-Lex.gz -INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing +$(LOG)/HOL-Lex.gz: $(OUT)/HOL Lex/Auto.thy Lex/Auto.ML \ + Lex/AutoChopper.thy Lex/AutoChopper.ML Lex/AutoChopper1.thy \ + Lex/Chopper.thy Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \ + Lex/Regset_of_auto.ML Lex/Regset_of_auto.thy + @$(ISATOOL) usedir $(OUT)/HOL Lex -INTEG_FILES = Integ/ROOT.ML \ - $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) + +## HOL-Integ + +HOL-Integ: HOL $(LOG)/HOL-Integ.gz -$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES) +$(LOG)/HOL-Integ.gz: $(OUT)/HOL Integ/Bin.ML Integ/Bin.thy \ + Integ/Equiv.ML Integ/Equiv.thy Integ/Group.ML Integ/Group.thy \ + Integ/IntRing.ML Integ/IntRing.thy Integ/IntRingDefs.ML \ + Integ/IntRingDefs.thy Integ/Integ.ML Integ/Integ.thy Integ/Lagrange.ML \ + Integ/Lagrange.thy Integ/ROOT.ML Integ/Ring.ML Integ/Ring.thy @$(ISATOOL) usedir $(OUT)/HOL Integ -## TLA -- Temporal Logic of Actions - -TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \ - TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \ - TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML - -TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy - -TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \ - TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML +## HOL-Auth -TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \ - TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \ - TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \ - TLA/Memory/Memory.ML TLA/Memory/Memory.thy \ - TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \ - TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \ - TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \ - TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \ - TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy - - -$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES) - @cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA +HOL-Auth: HOL $(LOG)/HOL-Auth.gz -$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES) - @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc - -$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES) - @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer - -$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES) - @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory - - -## I/O Automata (meta theory only) - -IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \ - IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML - -$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES) - @$(ISATOOL) usedir $(OUT)/HOL IOA - - -## Authentication & Security Protocols - -AUTH_NAMES = Message Event Shared NS_Shared \ - OtwayRees OtwayRees_AN OtwayRees_Bad \ - Recur WooLam Yahalom Yahalom2 \ - Public NS_Public_Bad NS_Public TLS - -AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) - -$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES) +$(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event.ML Auth/Event.thy \ + Auth/Message.ML Auth/Message.thy Auth/NS_Public.ML Auth/NS_Public.thy \ + Auth/NS_Public_Bad.ML Auth/NS_Public_Bad.thy Auth/NS_Shared.ML \ + Auth/NS_Shared.thy Auth/OtwayRees.ML Auth/OtwayRees.thy \ + Auth/OtwayRees_AN.ML Auth/OtwayRees_AN.thy Auth/OtwayRees_Bad.ML \ + Auth/OtwayRees_Bad.thy Auth/Public.ML Auth/Public.thy Auth/ROOT.ML \ + Auth/Recur.ML Auth/Recur.thy Auth/Shared.ML Auth/Shared.thy \ + Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \ + Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy @$(ISATOOL) usedir $(OUT)/HOL Auth -## Modelchecker invocation +## HOL-Modelcheck + +HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz -MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \ - Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \ - Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML - -$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES) +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ + Modelcheck/Example.ML Modelcheck/Example.thy Modelcheck/MCSyn.ML \ + Modelcheck/MCSyn.thy Modelcheck/MuCalculus.ML \ + Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL Modelcheck -## Properties of substitutions - -SUBST_NAMES = AList Subst Unifier UTerm Unify +## HOL-Lambda -SUBST_FILES = Subst/ROOT.ML \ - $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) - -$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES) - @$(ISATOOL) usedir $(OUT)/HOL Subst +HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz - -## Confluence of Lambda-calculus - -LAMBDA_NAMES = Lambda ParRed Commutation Eta - -LAMBDA_FILES = Lambda/ROOT.ML \ - $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) - -$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES) +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \ + Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy Lambda/Lambda.ML \ + Lambda/Lambda.thy Lambda/ParRed.ML Lambda/ParRed.thy Lambda/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL Lambda -## Type inference without let +## HOL-W0 -W0_NAMES = I Maybe MiniML Type W +HOL-W0: HOL $(LOG)/HOL-W0.gz -W0_FILES = W0/ROOT.ML \ - $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML) - -$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES) +$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/I.ML W0/I.thy W0/Maybe.ML W0/Maybe.thy \ + W0/MiniML.ML W0/MiniML.thy W0/ROOT.ML W0/Type.ML W0/Type.thy W0/W.ML \ + W0/W.thy @$(ISATOOL) usedir $(OUT)/HOL W0 -## Type inference with let +## HOL-MiniML -MINIML_NAMES = Generalize Instance Maybe MiniML Type W +HOL-MiniML: HOL $(LOG)/HOL-MiniML.gz -MINIML_FILES = MiniML/ROOT.ML \ - $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) - -$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES) +$(LOG)/HOL-MiniML.gz: $(OUT)/HOL MiniML/Generalize.ML \ + MiniML/Generalize.thy MiniML/Instance.ML MiniML/Instance.thy \ + MiniML/Maybe.ML MiniML/Maybe.thy MiniML/MiniML.ML MiniML/MiniML.thy \ + MiniML/ROOT.ML MiniML/Type.ML MiniML/Type.thy MiniML/W.ML MiniML/W.thy @$(ISATOOL) usedir $(OUT)/HOL MiniML -## Lexical analysis +## HOL-IOA + +HOL-IOA: HOL $(LOG)/HOL-IOA.gz -LEX_FILES = Auto AutoChopper Chopper Prefix +$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.ML IOA/Asig.thy IOA/IOA.ML \ + IOA/IOA.thy IOA/ROOT.ML IOA/Solve.ML IOA/Solve.thy + @$(ISATOOL) usedir $(OUT)/HOL IOA + + +## HOL-AxClasses + +HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz -LEX_FILES = Lex/ROOT.ML \ - $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) +$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/ROOT.ML + @$(ISATOOL) usedir $(OUT)/HOL AxClasses + + +## HOL-AxClasses-Group -$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES) - @$(ISATOOL) usedir $(OUT)/HOL Lex +HOL-AxClasses-Group: HOL-AxClasses $(LOG)/HOL-AxClasses-Group.gz + +$(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \ + AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \ + AxClasses/Group/GroupDefs.thy AxClasses/Group/GroupInsts.thy \ + AxClasses/Group/Monoid.thy AxClasses/Group/MonoidGroupInsts.thy \ + AxClasses/Group/ROOT.ML AxClasses/Group/Sigs.thy + @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group -## Axiomatic type classes examples - -AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \ - GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy +## HOL-AxClasses-Lattice -AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \ - LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \ - Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \ - Order.ML Order.thy ROOT.ML tools.ML +HOL-AxClasses-Lattice: HOL-AxClasses $(LOG)/HOL-AxClasses-Lattice.gz -AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \ - MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \ - ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \ - Xor.ML Xor.thy - -$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL - @$(ISATOOL) usedir $(OUT)/HOL AxClasses - -$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \ - $(AXC_GROUP_FILES:%=AxClasses/Group/%) - @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group - -$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \ - $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) +$(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \ + AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \ + AxClasses/Lattice/LatInsts.thy AxClasses/Lattice/LatMorph.ML \ + AxClasses/Lattice/LatMorph.thy AxClasses/Lattice/LatPreInsts.ML \ + AxClasses/Lattice/LatPreInsts.thy AxClasses/Lattice/Lattice.ML \ + AxClasses/Lattice/Lattice.thy AxClasses/Lattice/OrdDefs.ML \ + AxClasses/Lattice/OrdDefs.thy AxClasses/Lattice/OrdInsts.thy \ + AxClasses/Lattice/Order.ML AxClasses/Lattice/Order.thy \ + AxClasses/Lattice/ROOT.ML AxClasses/Lattice/tools.ML @$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice -$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \ - $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) + +## HOL-AxClasses-Tutorial + +HOL-AxClasses-Tutorial: HOL-AxClasses $(LOG)/HOL-AxClasses-Tutorial.gz + +$(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \ + AxClasses/Tutorial/BoolGroupInsts.thy AxClasses/Tutorial/Group.ML \ + AxClasses/Tutorial/Group.thy AxClasses/Tutorial/Monoid.thy \ + AxClasses/Tutorial/MonoidGroupInsts.thy \ + AxClasses/Tutorial/ProdGroupInsts.thy AxClasses/Tutorial/Product.thy \ + AxClasses/Tutorial/ProductInsts.thy AxClasses/Tutorial/ROOT.ML \ + AxClasses/Tutorial/Semigroup.thy AxClasses/Tutorial/Semigroups.thy \ + AxClasses/Tutorial/Sigs.thy AxClasses/Tutorial/Xor.ML \ + AxClasses/Tutorial/Xor.thy @$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial -## Higher-order quotients and example fractionals +## HOL-Quot + +HOL-Quot: HOL $(LOG)/HOL-Quot.gz -QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \ - Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \ - Quot/FRACT.thy Quot/FRACT.ML - -$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES) +$(LOG)/HOL-Quot.gz: $(OUT)/HOL Quot/FRACT.ML Quot/FRACT.thy \ + Quot/HQUOT.ML Quot/HQUOT.thy Quot/NPAIR.ML Quot/NPAIR.thy Quot/PER.ML \ + Quot/PER.thy Quot/PER0.ML Quot/PER0.thy Quot/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL Quot -## Miscellaneous examples +## HOL-ex -EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT +HOL-ex: HOL $(LOG)/HOL-ex.gz -EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ - ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) - -$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES) +$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/BT.ML ex/BT.thy ex/Fib.ML ex/Fib.thy \ + ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \ + ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML ex/Primrec.thy \ + ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML \ + ex/Recdef.ML ex/Recdef.thy ex/String.ML ex/String.thy ex/cla.ML \ + ex/meson.ML ex/mesontest.ML ex/rel.ML ex/set.ML @$(ISATOOL) usedir $(OUT)/HOL ex -## Full test +## TLA + +TLA: HOL $(OUT)/TLA + +$(OUT)/TLA: $(OUT)/HOL TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \ + TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \ + TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML + @cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA + + +## TLA-Inc + +TLA-Inc: TLA $(LOG)/TLA-Inc.gz + +$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy TLA/Inc/Inc.ML \ + TLA/Inc/Pcount.thy + @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc + + +## TLA-Buffer + +TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz -ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \ - $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \ - $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \ - $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ - $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \ - $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \ - $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \ - $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz +$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \ + TLA/Buffer/Buffer.ML TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML + @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer + + +## TLA-Memory + +TLA-Memory: TLA $(LOG)/TLA-Memory.gz -test: $(ALL_TARGETS) +$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MIParameters.thy \ + TLA/Memory/MIlive.ML TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML \ + TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.ML \ + TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.ML \ + TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.ML \ + TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.ML \ + TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.ML \ + TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.ML TLA/Memory/RPC.thy \ + TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.ML \ + TLA/Memory/RPCParameters.thy + @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory + + +## clean clean: - @rm -f $(ALL_TARGETS) - - -.PRECIOUS: $(OUT)/Pure $(OUT)/HOL + @rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \ + $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \ + $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz \ + $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \ + $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \ + $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \ + $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \ + $(LOG)/HOL-ex.gz $(OUT)/TLA $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz \ + $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz diff -r fad9b7479dbe -r 74c01296e818 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/HOLCF/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,43 +4,69 @@ # IsaMakefile for HOLCF # -#### Base system +## targets +default: HOLCF +images: HOLCF IOA +test: HOLCF-IMP HOLCF-ex IOA-ABP IOA-NTP +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -THYS = Porder.thy Porder0.thy Pcpo.thy \ - Fun1.thy Fun2.thy Fun3.thy \ - Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ - Cprod1.thy Cprod2.thy Cprod3.thy \ - Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ - Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ - Up1.thy Up2.thy Up3.thy Fix.thy \ - One.thy Tr.thy\ - Discrete0.thy Discrete1.thy Discrete.thy\ - Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy + +## HOLCF + +HOLCF: HOL $(OUT)/HOLCF + +HOL: + @cd $(SRC)/HOL; $(ISATOOL) make HOL -ONLYTHYS = - -FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \ - holcf_logic.ML cont_consts.ML \ - domain/library.ML domain/syntax.ML domain/axioms.ML \ - domain/theorems.ML domain/extender.ML domain/interface.ML - -$(OUT)/HOLCF: $(OUT)/HOL $(FILES) +$(OUT)/HOLCF: $(OUT)/HOL Cfun1.ML Cfun1.thy Cfun2.ML Cfun2.thy \ + Cfun3.ML Cfun3.thy Cont.ML Cont.thy Cprod1.ML Cprod1.thy Cprod2.ML \ + Cprod2.thy Cprod3.ML Cprod3.thy Discrete.ML Discrete.thy Discrete0.ML \ + Discrete0.thy Discrete1.ML Discrete1.thy Fix.ML Fix.thy Fun1.ML \ + Fun1.thy Fun2.ML Fun2.thy Fun3.ML Fun3.thy HOLCF.ML HOLCF.thy Lift.ML \ + Lift.thy Lift1.ML Lift1.thy Lift2.ML Lift2.thy Lift3.ML Lift3.thy \ + One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy Porder0.ML \ + Porder0.thy ROOT.ML Sprod0.ML Sprod0.thy Sprod1.ML Sprod1.thy \ + Sprod2.ML Sprod2.thy Sprod3.ML Sprod3.thy Ssum0.ML Ssum0.thy Ssum1.ML \ + Ssum1.thy Ssum2.ML Ssum2.thy Ssum3.ML Ssum3.thy Tr.ML Tr.thy Up1.ML \ + Up1.thy Up2.ML Up2.thy Up3.ML Up3.thy adm.ML cont_consts.ML \ + domain/axioms.ML domain/extender.ML domain/interface.ML \ + domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML @$(ISATOOL) usedir -b $(OUT)/HOL HOLCF -$(OUT)/HOL: - @cd ../HOL; $(ISATOOL) make + +## HOLCF-IMP +HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz + +$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/Denotational.ML \ + IMP/Denotational.thy IMP/ROOT.ML + @$(ISATOOL) usedir $(OUT)/HOLCF IMP -#### Tests and examples +## HOLCF-ex + +HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz -## IOA meta theory and examples +$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \ + ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \ + ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \ + ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML + @$(ISATOOL) usedir $(OUT)/HOLCF ex -IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \ +## IOA + +IOA: HOLCF $(OUT)/IOA + +$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \ IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \ IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \ @@ -54,72 +80,41 @@ IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \ IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \ IOA/meta_theory/Compositionality.thy - - -IOA_ABP_FILES = IOA/ABP/Abschannel.thy \ - IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \ - IOA/ABP/Action.thy IOA/ABP/Check.ML \ - IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \ - IOA/ABP/Env.thy IOA/ABP/Impl.thy \ - IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \ - IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ - IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \ - IOA/ABP/Sender.thy IOA/ABP/Spec.thy + @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA -IOA_NTP_FILES = IOA/NTP/Abschannel.ML \ - IOA/NTP/Abschannel.thy IOA/NTP/Action.ML \ - IOA/NTP/Action.thy IOA/NTP/Correctness.ML \ - IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \ - IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \ - IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \ - IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \ - IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \ - IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \ - IOA/NTP/Sender.ML IOA/NTP/Sender.thy \ - IOA/NTP/Spec.thy +## IOA-ABP + +IOA-ABP: IOA $(LOG)/IOA-ABP.gz - -$(OUT)/IOA: $(OUT)/HOLCF $(IOA_FILES) - @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA - -$(LOG)/IOA-ABP.gz: $(OUT)/IOA $(IOA_ABP_FILES) +$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \ + IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML IOA/ABP/Action.thy \ + IOA/ABP/Check.ML IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \ + IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ + IOA/ABP/Lemmas.ML IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ + IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ + IOA/ABP/Spec.thy @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP -$(LOG)/IOA-NTP.gz: $(OUT)/IOA $(IOA_NTP_FILES) + +## IOA-NTP + +IOA-NTP: IOA $(LOG)/IOA-NTP.gz + +$(LOG)/IOA-NTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \ + IOA/NTP/Abschannel.thy IOA/NTP/Action.ML IOA/NTP/Action.thy \ + IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \ + IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \ + IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \ + IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.ML \ + IOA/NTP/Receiver.thy IOA/NTP/Sender.ML IOA/NTP/Sender.thy \ + IOA/NTP/Spec.thy @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP -## IMP - -IMP_THYS = IMP/Denotational.thy -IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) - -$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF $(IMP_FILES) - @$(ISATOOL) usedir $(OUT)/HOLCF IMP - - -## Miscellaneous examples - -EX_THYS = ex/Dnat.thy ex/Stream.thy \ - ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \ - ex/Hoare.thy ex/Loop.thy - -EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) - -$(LOG)/HOLCF-ex.gz: ex/ROOT.ML $(EX_FILES) - @$(ISATOOL) usedir $(OUT)/HOLCF ex - - -## Full test - -ALL_TARGETS = $(OUT)/HOLCF $(OUT)/IOA $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ - $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz - -test: $(ALL_TARGETS) +## clean clean: - @rm -f $(ALL_TARGETS) - - -.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF + @rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ + $(LOG)/HOLCF-ex.gz $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \ + $(LOG)/IOA-NTP.gz diff -r fad9b7479dbe -r 74c01296e818 src/LCF/IsaMakefile --- a/src/LCF/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/LCF/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,24 +4,41 @@ # IsaMakefile for LCF # +## targets + +default: LCF +images: LCF +test: LCF-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -FILES = ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML + +## LCF + +LCF: FOL $(OUT)/LCF -$(OUT)/LCF: $(OUT)/FOL $(FILES) +FOL: + @cd $(SRC)/FOL; $(ISATOOL) make FOL + +$(OUT)/LCF: $(OUT)/FOL LCF.ML LCF.thy ROOT.ML fix.ML pair.ML simpdata.ML @$(ISATOOL) usedir -b $(OUT)/FOL LCF -$(OUT)/FOL: - @cd ../FOL; $(ISATOOL) make + +## LCF-ex -$(LOG)/LCF-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/LCF +LCF-ex: LCF $(LOG)/LCF-ex.gz + +$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/ROOT.ML ex/ex.ML @$(ISATOOL) usedir $(OUT)/LCF ex -test: $(OUT)/LCF $(LOG)/LCF-ex.gz + +## clean clean: - @rm -f $(OUT)/LCF $(LOG)/LCF-ex.gz - - -.PRECIOUS: $(OUT)/FOL $(OUT)/LCF + @rm -f $(OUT)/LCF $(LOG)/LCF.gz $(LOG)/LCF-ex.gz diff -r fad9b7479dbe -r 74c01296e818 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/Pure/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -1,38 +1,51 @@ -# -# $Id$ # -# IsaMakefile for Pure Isabelle +# $Id$ # -# The Pure part is common to all systems. Object-logics (like FOL) -# are loaded on top of it. +# IsaMakefile for Pure # +## targets + +default: Pure +images: Pure +test: +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + -FILES = ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \ - ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \ - Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/pretty.ML \ - Syntax/printer.ML Syntax/symbol_font.ML Syntax/syn_ext.ML \ - Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \ - Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/file.ML \ - Thy/path.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML \ - Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \ - axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \ - goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \ - pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \ - sorts.ML table.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \ - type.ML type_infer.ML unify.ML +## Pure + +Pure: $(OUT)/Pure -$(OUT)/Pure: $(FILES) +$(OUT)/Pure: ML-Systems/mlworks.ML ML-Systems/polyml.ML \ + ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \ + Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ + Syntax/pretty.ML Syntax/printer.ML Syntax/symbol_font.ML \ + Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ + Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \ + Thy/browser_info.ML Thy/context.ML Thy/file.ML Thy/path.ML \ + Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML \ + Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML \ + display.ML drule.ML envir.ML goals.ML install_pp.ML library.ML \ + logic.ML name_space.ML net.ML pattern.ML pure_thy.ML search.ML \ + section_utils.ML seq.ML sign.ML sorts.ML table.ML tactic.ML tctical.ML \ + term.ML theory.ML thm.ML type.ML type_infer.ML unify.ML @./mk -RAW: $(FILES) + +## RAW + +RAW: @./mk -r -test: $(OUT)/Pure + +## clean clean: - @rm -f $(OUT)/Pure $(OUT)/RAW - - -.PRECIOUS: $(OUT)/Pure $(OUT)/RAW + @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz diff -r fad9b7479dbe -r 74c01296e818 src/Sequents/IsaMakefile --- a/src/Sequents/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/Sequents/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,32 +4,46 @@ # IsaMakefile for Sequents # +## targets + +default: Sequents +images: Sequents +test: Sequents-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -NAMES = ILL LK S4 S43 T -FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML) + +## Sequents + +Sequents: Pure $(OUT)/Sequents -ILL_NAMES = ILL_predlog washing -EX_FILES = ex/ROOT.ML \ - ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \ - ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \ - ex/ILL/ILL_kleene_lemmas.ML \ - $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML) +Pure: + @cd $(SRC)/Pure; $(ISATOOL) make Pure -$(OUT)/Sequents: $(OUT)/Pure $(FILES) +$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK.ML LK.thy ROOT.ML S4.ML \ + S4.thy S43.ML S43.thy Sequents.thy T.ML T.thy prover.ML @$(ISATOOL) usedir -b $(OUT)/Pure Sequents -$(OUT)/Pure: - @cd ../Pure; $(ISATOOL) make + +## Sequents-ex + +Sequents-ex: Sequents $(LOG)/Sequents-ex.gz -$(LOG)/Sequents-ex.gz: $(OUT)/Sequents $(EX_FILES) +$(LOG)/Sequents-ex.gz: $(OUT)/Sequents ex/ILL/ILL_kleene_lemmas.ML \ + ex/ILL/ILL_predlog.ML ex/ILL/ILL_predlog.thy ex/ILL/washing.ML \ + ex/ILL/washing.thy ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML \ + ex/LK/quant.ML ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML \ + ex/Modal/Tthms.ML ex/ROOT.ML @$(ISATOOL) usedir $(OUT)/Sequents ex -test: $(OUT)/Sequents $(LOG)/Sequents-ex.gz + +## clean clean: - @rm -f $(OUT)/Sequents $(LOG)/Sequents-ex.gz - - -.PRECIOUS: $(OUT)/Pure $(OUT)/Sequents + @rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ex.gz diff -r fad9b7479dbe -r 74c01296e818 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Tue Jan 06 12:32:43 1998 +0100 +++ b/src/ZF/IsaMakefile Wed Jan 07 13:53:42 1998 +0100 @@ -4,100 +4,118 @@ # IsaMakefile for ZF # -#### Base system +## targets +default: ZF +images: ZF +test: ZF-IMP ZF-Coind ZF-AC ZF-Resid ZF-ex +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -NAMES = ZF upair subset pair domrange \ - func AC equalities Bool \ - Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \ - constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \ - WF Order Ordinal Epsilon Arith Univ \ - QUniv Datatype OrderArith OrderType \ - Cardinal CardinalArith Cardinal_AC InfDatatype \ - Zorn Nat Finite List + +## ZF + +ZF: FOL $(OUT)/ZF + +FOL: + @cd $(SRC)/FOL; $(ISATOOL) make FOL -FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \ - $(NAMES:%=%.thy) $(NAMES:%=%.ML) - -$(OUT)/ZF: $(OUT)/FOL $(FILES) +$(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \ + Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ + CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \ + Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy EquivClass.ML \ + EquivClass.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \ + Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy List.ML \ + List.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \ + OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \ + Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \ + Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy WF.ML \ + WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \ + cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \ + domrange.thy equalities.ML equalities.thy func.ML func.thy \ + ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \ + intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \ + subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy @$(ISATOOL) usedir -b $(OUT)/FOL ZF -$(OUT)/FOL: - @cd ../FOL; $(ISATOOL) make - - -#### Tests and examples +## ZF-IMP -## IMP-semantics example +ZF-IMP: ZF $(LOG)/ZF-IMP.gz -IMP_NAMES = Com Denotation Equiv -IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) - -$(LOG)/ZF-IMP.gz: $(OUT)/ZF $(IMP_FILES) +$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \ + IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML @$(ISATOOL) usedir $(OUT)/ZF IMP -## Coinduction example +## ZF-Coind -COIND_NAMES = ECR MT Map Static Types Values +ZF-Coind: ZF $(LOG)/ZF-Coind.gz -COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \ - $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML) - -$(LOG)/ZF-Coind.gz: $(OUT)/ZF $(COIND_FILES) +$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \ + Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \ + Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \ + Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \ + Coind/Values.thy @$(ISATOOL) usedir $(OUT)/ZF Coind -## AC examples +## ZF-AC -AC_NAMES = AC_Equiv Cardinal_aux \ - AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \ - DC DC_lemmas HH Hartog WO1_AC \ - WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun +ZF-AC: ZF $(LOG)/ZF-AC.gz -AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \ - AC/AC2_AC6.ML AC/AC7_AC9.ML \ - AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \ - $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML) - -$(LOG)/ZF-AC.gz: $(OUT)/ZF $(AC_FILES) +$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/AC0_AC1.ML AC/AC10_AC15.ML \ + AC/AC15_WO6.ML AC/AC15_WO6.thy AC/AC16_WO4.ML AC/AC16_WO4.thy \ + AC/AC16_lemmas.ML AC/AC16_lemmas.thy AC/AC17_AC1.ML AC/AC17_AC1.thy \ + AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_AC17.ML AC/AC1_WO2.ML \ + AC/AC1_WO2.thy AC/AC2_AC6.ML AC/AC7_AC9.ML AC/AC_Equiv.ML \ + AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \ + AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \ + AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \ + AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML AC/WO2_AC16.ML \ + AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \ + AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy @$(ISATOOL) usedir $(OUT)/ZF AC -## Residuals example +## ZF-Resid + +ZF-Resid: ZF $(LOG)/ZF-Resid.gz -RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \ - Cube Residuals Terms - -RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML) - -$(LOG)/ZF-Resid.gz: $(OUT)/ZF $(RESID_FILES) +$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \ + Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \ + Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \ + Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \ + Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \ + Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy @$(ISATOOL) usedir $(OUT)/ZF Resid -## Miscellaneous examples +## ZF-ex + +ZF-ex: ZF $(LOG)/ZF-ex.gz -EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \ - Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit - -EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) - -$(LOG)/ZF-ex.gz: $(OUT)/ZF $(EX_FILES) +$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ + ex/Bin.ML ex/Bin.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ + ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ + ex/Enum.thy ex/Integ.ML ex/Integ.thy ex/LList.ML ex/LList.thy \ + ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ + ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ + ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ + ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ + ex/Term.ML ex/Term.thy ex/misc.ML ex/twos_compl.ML ex/twos_compl.thy @$(ISATOOL) usedir $(OUT)/ZF ex -## Full test - -ALL_TARGETS = $(OUT)/ZF $(LOG)/ZF-IMP.gz $(LOG)/ZF-Coind.gz \ - $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz $(LOG)/ZF-ex.gz - -test: $(ALL_TARGETS) +## clean clean: - @rm -f $(ALL_TARGETS) - - -.PRECIOUS: $(OUT)/FOL $(OUT)/ZF + @rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-IMP.gz \ + $(LOG)/ZF-Coind.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz \ + $(LOG)/ZF-ex.gz