improved targets;
authorwenzelm
Wed Jan 07 13:53:42 1998 +0100 (1998-01-07 ago)
changeset 451874c01296e818
parent 4517 fad9b7479dbe
child 4519 055f2067d373
improved targets;
fixed dependencies on parent logics;
src/CCL/IsaMakefile
src/CTT/IsaMakefile
src/Cube/IsaMakefile
src/FOL/IsaMakefile
src/FOLP/IsaMakefile
src/HOL/IsaMakefile
src/HOLCF/IsaMakefile
src/LCF/IsaMakefile
src/Pure/IsaMakefile
src/Sequents/IsaMakefile
src/ZF/IsaMakefile
     1.1 --- a/src/CCL/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     1.2 +++ b/src/CCL/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     1.3 @@ -4,33 +4,46 @@
     1.4  # IsaMakefile for CCL
     1.5  #
     1.6  
     1.7 +## targets
     1.8 +
     1.9 +default: CCL
    1.10 +images: CCL
    1.11 +test: CCL-ex
    1.12 +all: images test
    1.13 +
    1.14 +
    1.15 +## global settings
    1.16 +
    1.17 +SRC = $(ISABELLE_HOME)/src
    1.18  OUT = $(ISABELLE_OUTPUT)
    1.19  LOG = $(OUT)/log
    1.20  
    1.21 -SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
    1.22 -	    Gfp.thy Gfp.ML Lfp.thy Lfp.ML
    1.23 +
    1.24 +## CCL
    1.25 +
    1.26 +CCL: FOL $(OUT)/CCL
    1.27  
    1.28 -CCL_FILES = CCL.thy CCL.ML Term.thy Term.ML Type.thy Type.ML \
    1.29 -	    coinduction.ML Hered.thy Hered.ML Trancl.thy Trancl.ML \
    1.30 -	    Wfd.thy Wfd.ML genrec.ML typecheck.ML eval.ML Fix.thy Fix.ML
    1.31 +FOL:
    1.32 +	@cd $(SRC)/FOL; $(ISATOOL) make FOL
    1.33  
    1.34 -EX_FILES = ex/ROOT.ML ex/Flag.ML ex/Flag.thy ex/List.ML ex/List.thy \
    1.35 -	   ex/Nat.ML ex/Nat.thy ex/Stream.ML ex/Stream.thy
    1.36 -
    1.37 -
    1.38 -$(OUT)/CCL: $(OUT)/FOL $(SET_FILES) $(CCL_FILES)
    1.39 +$(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \
    1.40 +  Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \
    1.41 +  Term.thy Trancl.ML Trancl.thy Type.ML Type.thy Wfd.ML Wfd.thy \
    1.42 +  coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \
    1.43 +  typecheck.ML
    1.44  	@$(ISATOOL) usedir -b $(OUT)/FOL CCL
    1.45  
    1.46 -$(OUT)/FOL:
    1.47 -	@cd ../FOL; $(ISATOOL) make
    1.48 +
    1.49 +## CCL-ex
    1.50  
    1.51 -$(LOG)/CCL-ex.gz: ex/ROOT.ML $(OUT)/CCL $(EX_FILES)
    1.52 +CCL-ex: CCL $(LOG)/CCL-ex.gz
    1.53 +
    1.54 +$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.ML ex/Flag.thy ex/List.ML \
    1.55 +  ex/List.thy ex/Nat.ML ex/Nat.thy ex/ROOT.ML ex/Stream.ML ex/Stream.thy
    1.56  	@$(ISATOOL) usedir $(OUT)/CCL ex
    1.57  
    1.58 -test: $(OUT)/CCL $(LOG)/CCL-ex.gz
    1.59 +
    1.60 +## clean
    1.61  
    1.62  clean:
    1.63 -	@rm -f $(OUT)/CCL $(LOG)/CCL-ex.gz
    1.64 -
    1.65 -
    1.66 -.PRECIOUS: $(OUT)/FOL $(OUT)/CCL
    1.67 +	@rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz
     2.1 --- a/src/CTT/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     2.2 +++ b/src/CTT/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     2.3 @@ -4,27 +4,43 @@
     2.4  # IsaMakefile for CTT
     2.5  #
     2.6  
     2.7 +## targets
     2.8 +
     2.9 +default: CTT
    2.10 +images: CTT
    2.11 +test: CTT-ex
    2.12 +all: images test
    2.13 +
    2.14 +
    2.15 +## global settings
    2.16 +
    2.17 +SRC = $(ISABELLE_HOME)/src
    2.18  OUT = $(ISABELLE_OUTPUT)
    2.19  LOG = $(OUT)/log
    2.20  
    2.21 -FILES =	ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
    2.22 -	Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML
    2.23 +
    2.24 +## CTT
    2.25 +
    2.26 +CTT: Pure $(OUT)/CTT
    2.27  
    2.28 -EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
    2.29 +Pure:
    2.30 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    2.31  
    2.32 -$(OUT)/CTT: $(OUT)/Pure $(FILES)
    2.33 +$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \
    2.34 +  Bool.ML Bool.thy CTT.ML CTT.thy ROOT.ML rew.ML
    2.35  	@$(ISATOOL) usedir -b $(OUT)/Pure CTT
    2.36  
    2.37 -$(OUT)/Pure:
    2.38 -	@cd ../Pure; $(ISATOOL) make
    2.39 +
    2.40 +## CTT-ex
    2.41  
    2.42 -$(LOG)/CTT-ex.gz: ex/ROOT.ML $(OUT)/CTT $(EX_FILES)
    2.43 +CTT-ex: CTT $(LOG)/CTT-ex.gz
    2.44 +
    2.45 +$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/elim.ML ex/equal.ML \
    2.46 +  ex/synth.ML ex/typechk.ML
    2.47  	@$(ISATOOL) usedir $(OUT)/CTT ex
    2.48  
    2.49 -test: $(OUT)/CTT $(LOG)/CTT-ex.gz
    2.50 +
    2.51 +## clean
    2.52  
    2.53  clean:
    2.54 -	@rm -f $(OUT)/CTT $(LOG)/CTT-ex.gz
    2.55 -
    2.56 -
    2.57 -.PRECIOUS: $(OUT)/Pure $(OUT)/CTT
    2.58 +	@rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz
     3.1 --- a/src/Cube/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     3.2 +++ b/src/Cube/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     3.3 @@ -4,24 +4,41 @@
     3.4  # IsaMakefile for Cube
     3.5  #
     3.6  
     3.7 +## targets
     3.8 +
     3.9 +default: Cube
    3.10 +images: Cube
    3.11 +test: Cube-ex
    3.12 +all: images test
    3.13 +
    3.14 +
    3.15 +## global settings
    3.16 +
    3.17 +SRC = $(ISABELLE_HOME)/src
    3.18  OUT = $(ISABELLE_OUTPUT)
    3.19  LOG = $(OUT)/log
    3.20  
    3.21 -FILES =	ROOT.ML Cube.thy Cube.ML
    3.22 +
    3.23 +## Cube
    3.24 +
    3.25 +Cube: Pure $(OUT)/Cube
    3.26  
    3.27 -$(OUT)/Cube: $(OUT)/Pure $(FILES)
    3.28 +Pure:
    3.29 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    3.30 +
    3.31 +$(OUT)/Cube: $(OUT)/Pure Cube.ML Cube.thy ROOT.ML
    3.32  	@$(ISATOOL) usedir -b $(OUT)/Pure Cube
    3.33  
    3.34 -$(OUT)/Pure:
    3.35 -	@cd ../Pure; $(ISATOOL) make
    3.36 +
    3.37 +## Cube-ex
    3.38  
    3.39 -$(LOG)/Cube-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/Cube
    3.40 +Cube-ex: Cube $(LOG)/Cube-ex.gz
    3.41 +
    3.42 +$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ROOT.ML
    3.43  	@$(ISATOOL) usedir $(OUT)/Cube ex
    3.44  
    3.45 -test: $(OUT)/Cube $(LOG)/Cube-ex.gz
    3.46 +
    3.47 +## clean
    3.48  
    3.49  clean:
    3.50 -	@rm -f $(OUT)/Cube $(LOG)/Cube-ex.gz
    3.51 -
    3.52 -
    3.53 -.PRECIOUS: $(OUT)/Pure $(OUT)/Cube
    3.54 +	@rm -f $(OUT)/Cube $(LOG)/Cube.gz $(LOG)/Cube-ex.gz
     4.1 --- a/src/FOL/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     4.2 +++ b/src/FOL/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     4.3 @@ -4,33 +4,48 @@
     4.4  # IsaMakefile for FOL
     4.5  #
     4.6  
     4.7 +## targets
     4.8 +
     4.9 +default: FOL
    4.10 +images: FOL
    4.11 +test: FOL-ex
    4.12 +all: images test
    4.13 +
    4.14 +
    4.15 +## global settings
    4.16 +
    4.17 +SRC = $(ISABELLE_HOME)/src
    4.18  OUT = $(ISABELLE_OUTPUT)
    4.19  LOG = $(OUT)/log
    4.20  
    4.21 -PROVERS = hypsubst.ML classical.ML blast.ML \
    4.22 -	simplifier.ML splitter.ML ind.ML 
    4.23  
    4.24 -FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    4.25 -	fologic.ML cladata.ML $(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%)
    4.26 +## FOL
    4.27 +
    4.28 +FOL: Pure $(OUT)/FOL
    4.29  
    4.30 -EX_NAMES = If List Nat Nat2 Prolog IffOracle
    4.31 -EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \
    4.32 -	   ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    4.33 +Pure:
    4.34 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    4.35  
    4.36 -
    4.37 -$(OUT)/FOL: $(OUT)/Pure $(FILES)
    4.38 +$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
    4.39 +  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \
    4.40 +  $(SRC)/Provers/ind.ML $(SRC)/Provers/simplifier.ML \
    4.41 +  $(SRC)/Provers/splitter.ML FOL.ML FOL.thy IFOL.ML IFOL.thy ROOT.ML \
    4.42 +  cladata.ML fologic.ML intprover.ML simpdata.ML
    4.43  	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
    4.44  
    4.45 -$(OUT)/Pure:
    4.46 -	@cd ../Pure; $(ISATOOL) make
    4.47 +
    4.48 +## FOL-ex
    4.49 +
    4.50 +FOL-ex: FOL $(LOG)/FOL-ex.gz
    4.51  
    4.52 -$(LOG)/FOL-ex.gz: ex/ROOT.ML $(OUT)/FOL $(EX_FILES)
    4.53 +$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/If.ML ex/If.thy ex/IffOracle.ML \
    4.54 +  ex/IffOracle.thy ex/List.ML ex/List.thy ex/Nat.ML ex/Nat.thy \
    4.55 +  ex/Nat2.ML ex/Nat2.thy ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/cla.ML \
    4.56 +  ex/foundn.ML ex/int.ML ex/intro.ML ex/prop.ML ex/quant.ML
    4.57  	@$(ISATOOL) usedir $(OUT)/FOL ex
    4.58  
    4.59 -test: $(OUT)/FOL $(LOG)/FOL-ex.gz
    4.60 +
    4.61 +## clean
    4.62  
    4.63  clean:
    4.64 -	@rm -f $(OUT)/FOL $(LOG)/FOL-ex.gz
    4.65 -
    4.66 -
    4.67 -.PRECIOUS: $(OUT)/Pure $(OUT)/FOL
    4.68 +	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz
     5.1 --- a/src/FOLP/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     5.2 +++ b/src/FOLP/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     5.3 @@ -4,29 +4,44 @@
     5.4  # IsaMakefile for FOLP
     5.5  #
     5.6  
     5.7 +## targets
     5.8 +
     5.9 +default: FOLP
    5.10 +images: FOLP
    5.11 +test: FOLP-ex
    5.12 +all: images test
    5.13 +
    5.14 +
    5.15 +## global settings
    5.16 +
    5.17 +SRC = $(ISABELLE_HOME)/src
    5.18  OUT = $(ISABELLE_OUTPUT)
    5.19  LOG = $(OUT)/log
    5.20  
    5.21 -FILES =	ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \
    5.22 -	hypsubst.ML classical.ML simp.ML
    5.23 +
    5.24 +## FOLP
    5.25 +
    5.26 +FOLP: Pure $(OUT)/FOLP
    5.27  
    5.28 -EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML \
    5.29 -	   ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy \
    5.30 -	   ex/prop.ML ex/quant.ML
    5.31 +Pure:
    5.32 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    5.33  
    5.34 -$(OUT)/FOLP: $(OUT)/Pure $(FILES)
    5.35 +$(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
    5.36 +  classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
    5.37  	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
    5.38  
    5.39 -$(OUT)/Pure:
    5.40 -	@cd ../Pure; $(ISATOOL) make
    5.41 +
    5.42 +## FOLP-ex
    5.43  
    5.44 -$(LOG)/FOLP-ex.gz: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES)
    5.45 +FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
    5.46 +
    5.47 +$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/foundn.ML \
    5.48 +  ex/If.ML ex/If.thy ex/int.ML ex/intro.ML ex/Nat.ML ex/Nat.thy \
    5.49 +  ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
    5.50  	@$(ISATOOL) usedir $(OUT)/FOLP ex
    5.51  
    5.52 -test: $(OUT)/FOLP $(LOG)/FOLP-ex.gz
    5.53 +
    5.54 +## clean
    5.55  
    5.56  clean:
    5.57 -	@rm -f $(OUT)/FOLP $(LOG)/FOLP-ex.gz
    5.58 -
    5.59 -
    5.60 -.PRECIOUS: $(OUT)/Pure $(OUT)/FOLP
    5.61 +	@rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz
     6.1 --- a/src/HOL/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     6.2 +++ b/src/HOL/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     6.3 @@ -4,267 +4,320 @@
     6.4  # IsaMakefile for HOL
     6.5  #
     6.6  
     6.7 -#### Base system
     6.8 +## targets
     6.9  
    6.10 +default: HOL
    6.11 +images: HOL TLA
    6.12 +test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Integ \
    6.13 +  HOL-Auth HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
    6.14 +  HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
    6.15 +  HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory
    6.16 +all: images test
    6.17 +
    6.18 +
    6.19 +## global settings
    6.20 +
    6.21 +SRC = $(ISABELLE_HOME)/src
    6.22  OUT = $(ISABELLE_OUTPUT)
    6.23  LOG = $(OUT)/log
    6.24  
    6.25 -NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
    6.26 -	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
    6.27 -	Divides Power Sexp Univ List RelPow Option Map
    6.28 +
    6.29 +## HOL
    6.30  
    6.31 -PROVERS = hypsubst.ML classical.ML blast.ML \
    6.32 -	simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML
    6.33 +HOL: Pure $(OUT)/HOL
    6.34 +
    6.35 +Pure:
    6.36 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    6.37  
    6.38 -TFL   = dcterm.sml post.sml rules.new.sml rules.sig \
    6.39 -	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
    6.40 -	usyntax.sig usyntax.sml utils.sig utils.sml
    6.41 -
    6.42 -FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    6.43 -	ind_syntax.ML cladata.ML record.ML simpdata.ML arith_data.ML \
    6.44 -	typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \
    6.45 -	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
    6.46 -	$(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%)
    6.47 -
    6.48 -$(OUT)/HOL: $(OUT)/Pure $(FILES)
    6.49 +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
    6.50 +  $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \
    6.51 +  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \
    6.52 +  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
    6.53 +  $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
    6.54 +  $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml \
    6.55 +  $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig \
    6.56 +  $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml \
    6.57 +  $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig \
    6.58 +  $(SRC)/TFL/utils.sml Arith.ML Arith.thy Divides.ML Divides.thy \
    6.59 +  Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    6.60 +  Inductive.ML Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML \
    6.61 +  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy \
    6.62 +  Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML \
    6.63 +  RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    6.64 +  Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy WF.ML WF.thy \
    6.65 +  WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \
    6.66 +  datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \
    6.67 +  indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \
    6.68 +  record.ML simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML \
    6.69 +  typedef.ML
    6.70  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    6.71  
    6.72 -$(OUT)/Pure:
    6.73 -	@cd ../Pure; $(ISATOOL) make
    6.74 +
    6.75 +## HOL-Subst
    6.76 +
    6.77 +HOL-Subst: HOL $(LOG)/HOL-Subst.gz
    6.78 +
    6.79 +$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.ML Subst/AList.thy \
    6.80 +  Subst/ROOT.ML Subst/Subst.ML Subst/Subst.thy Subst/UTerm.ML \
    6.81 +  Subst/UTerm.thy Subst/Unifier.ML Subst/Unifier.thy Subst/Unify.ML \
    6.82 +  Subst/Unify.thy
    6.83 +	@$(ISATOOL) usedir $(OUT)/HOL Subst
    6.84  
    6.85  
    6.86 -#### Tests and examples
    6.87 +## HOL-Induct
    6.88  
    6.89 -## Inductive definitions: simple examples
    6.90 +HOL-Induct: HOL $(LOG)/HOL-Induct.gz
    6.91  
    6.92 -INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult Com Exp
    6.93 -
    6.94 -INDUCT_FILES = Induct/ROOT.ML \
    6.95 -	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
    6.96 -
    6.97 -$(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES)
    6.98 +$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Acc.ML Induct/Acc.thy \
    6.99 +  Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   6.100 +  Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
   6.101 +  Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
   6.102 +  Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \
   6.103 +  Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/Simult.ML \
   6.104 +  Induct/Simult.thy Induct/Term.ML Induct/Term.thy
   6.105  	@$(ISATOOL) usedir $(OUT)/HOL Induct
   6.106  
   6.107  
   6.108 -## IMP-semantics example
   6.109 +## HOL-IMP
   6.110 +
   6.111 +HOL-IMP: HOL $(LOG)/HOL-IMP.gz
   6.112  
   6.113 -IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
   6.114 -IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
   6.115 -
   6.116 -$(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES)
   6.117 +$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
   6.118 +  IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
   6.119 +  IMP/Natural.ML IMP/Natural.thy IMP/ROOT.ML IMP/Transition.ML \
   6.120 +  IMP/Transition.thy IMP/VC.ML IMP/VC.thy
   6.121  	@$(ISATOOL) usedir $(OUT)/HOL IMP
   6.122  
   6.123  
   6.124 -## Hoare logic
   6.125 +## HOL-Hoare
   6.126 +
   6.127 +HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
   6.128  
   6.129 -Hoare_NAMES = Hoare Arith2 Examples
   6.130 -Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
   6.131 -	      $(Hoare_NAMES:%=Hoare/%.ML)
   6.132 -
   6.133 -$(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES)
   6.134 +$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \
   6.135 +  Hoare/Examples.ML Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \
   6.136 +  Hoare/ROOT.ML
   6.137  	@$(ISATOOL) usedir $(OUT)/HOL Hoare
   6.138  
   6.139  
   6.140 -## The integers in HOL
   6.141 +## HOL-Lex
   6.142 +
   6.143 +HOL-Lex: HOL $(LOG)/HOL-Lex.gz
   6.144  
   6.145 -INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
   6.146 +$(LOG)/HOL-Lex.gz: $(OUT)/HOL Lex/Auto.thy Lex/Auto.ML \
   6.147 +  Lex/AutoChopper.thy Lex/AutoChopper.ML Lex/AutoChopper1.thy \
   6.148 +  Lex/Chopper.thy Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \
   6.149 +  Lex/Regset_of_auto.ML Lex/Regset_of_auto.thy
   6.150 +	@$(ISATOOL) usedir $(OUT)/HOL Lex
   6.151  
   6.152 -INTEG_FILES = Integ/ROOT.ML \
   6.153 -	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
   6.154 +
   6.155 +## HOL-Integ
   6.156 +
   6.157 +HOL-Integ: HOL $(LOG)/HOL-Integ.gz
   6.158  
   6.159 -$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES)
   6.160 +$(LOG)/HOL-Integ.gz: $(OUT)/HOL Integ/Bin.ML Integ/Bin.thy \
   6.161 +  Integ/Equiv.ML Integ/Equiv.thy Integ/Group.ML Integ/Group.thy \
   6.162 +  Integ/IntRing.ML Integ/IntRing.thy Integ/IntRingDefs.ML \
   6.163 +  Integ/IntRingDefs.thy Integ/Integ.ML Integ/Integ.thy Integ/Lagrange.ML \
   6.164 +  Integ/Lagrange.thy Integ/ROOT.ML Integ/Ring.ML Integ/Ring.thy
   6.165  	@$(ISATOOL) usedir $(OUT)/HOL Integ
   6.166  
   6.167  
   6.168 -## TLA -- Temporal Logic of Actions
   6.169 -
   6.170 -TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \
   6.171 -	TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \
   6.172 -	TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML
   6.173 -
   6.174 -TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy
   6.175 -
   6.176 -TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \
   6.177 -	TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML
   6.178 +## HOL-Auth
   6.179  
   6.180 -TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \
   6.181 -	TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \
   6.182 -	TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \
   6.183 -	TLA/Memory/Memory.ML TLA/Memory/Memory.thy \
   6.184 -	TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \
   6.185 -	TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \
   6.186 -	TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \
   6.187 -	TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \
   6.188 -	TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy
   6.189 -
   6.190 -
   6.191 -$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES)
   6.192 -	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
   6.193 +HOL-Auth: HOL $(LOG)/HOL-Auth.gz
   6.194  
   6.195 -$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES)
   6.196 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
   6.197 -
   6.198 -$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES)
   6.199 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
   6.200 -
   6.201 -$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES)
   6.202 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
   6.203 -
   6.204 -
   6.205 -## I/O Automata (meta theory only)
   6.206 -
   6.207 -IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
   6.208 -  IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
   6.209 -
   6.210 -$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES)
   6.211 -	@$(ISATOOL) usedir $(OUT)/HOL IOA
   6.212 -
   6.213 -
   6.214 -## Authentication & Security Protocols
   6.215 -
   6.216 -AUTH_NAMES = Message Event Shared NS_Shared \
   6.217 -	     OtwayRees OtwayRees_AN OtwayRees_Bad \
   6.218 -	     Recur WooLam Yahalom Yahalom2 \
   6.219 -	     Public NS_Public_Bad NS_Public TLS
   6.220 -
   6.221 -AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
   6.222 -
   6.223 -$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES)
   6.224 +$(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event.ML Auth/Event.thy \
   6.225 +  Auth/Message.ML Auth/Message.thy Auth/NS_Public.ML Auth/NS_Public.thy \
   6.226 +  Auth/NS_Public_Bad.ML Auth/NS_Public_Bad.thy Auth/NS_Shared.ML \
   6.227 +  Auth/NS_Shared.thy Auth/OtwayRees.ML Auth/OtwayRees.thy \
   6.228 +  Auth/OtwayRees_AN.ML Auth/OtwayRees_AN.thy Auth/OtwayRees_Bad.ML \
   6.229 +  Auth/OtwayRees_Bad.thy Auth/Public.ML Auth/Public.thy Auth/ROOT.ML \
   6.230 +  Auth/Recur.ML Auth/Recur.thy Auth/Shared.ML Auth/Shared.thy \
   6.231 +  Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \
   6.232 +  Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy
   6.233  	@$(ISATOOL) usedir $(OUT)/HOL Auth
   6.234  
   6.235  
   6.236 -## Modelchecker invocation
   6.237 +## HOL-Modelcheck
   6.238 +
   6.239 +HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
   6.240  
   6.241 -MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \
   6.242 -  Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
   6.243 -  Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
   6.244 -
   6.245 -$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES)
   6.246 +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
   6.247 +  Modelcheck/Example.ML Modelcheck/Example.thy Modelcheck/MCSyn.ML \
   6.248 +  Modelcheck/MCSyn.thy Modelcheck/MuCalculus.ML	\
   6.249 +  Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
   6.250  	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
   6.251  
   6.252  
   6.253 -## Properties of substitutions
   6.254 -
   6.255 -SUBST_NAMES = AList Subst Unifier UTerm Unify
   6.256 +## HOL-Lambda
   6.257  
   6.258 -SUBST_FILES = Subst/ROOT.ML \
   6.259 -	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   6.260 -
   6.261 -$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES)
   6.262 -	@$(ISATOOL) usedir $(OUT)/HOL Subst
   6.263 +HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
   6.264  
   6.265 -
   6.266 -## Confluence of Lambda-calculus
   6.267 -
   6.268 -LAMBDA_NAMES = Lambda ParRed Commutation Eta
   6.269 -
   6.270 -LAMBDA_FILES = Lambda/ROOT.ML \
   6.271 -	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   6.272 -
   6.273 -$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES)
   6.274 +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \
   6.275 +  Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy Lambda/Lambda.ML \
   6.276 +  Lambda/Lambda.thy Lambda/ParRed.ML Lambda/ParRed.thy Lambda/ROOT.ML
   6.277  	@$(ISATOOL) usedir $(OUT)/HOL Lambda
   6.278  
   6.279  
   6.280 -## Type inference without let
   6.281 +## HOL-W0
   6.282  
   6.283 -W0_NAMES = I Maybe MiniML Type W
   6.284 +HOL-W0: HOL $(LOG)/HOL-W0.gz
   6.285  
   6.286 -W0_FILES = W0/ROOT.ML \
   6.287 -	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
   6.288 -
   6.289 -$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES)
   6.290 +$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/I.ML W0/I.thy W0/Maybe.ML W0/Maybe.thy \
   6.291 +  W0/MiniML.ML W0/MiniML.thy W0/ROOT.ML W0/Type.ML W0/Type.thy W0/W.ML \
   6.292 +  W0/W.thy
   6.293  	@$(ISATOOL) usedir $(OUT)/HOL W0
   6.294  
   6.295  
   6.296 -## Type inference with let
   6.297 +## HOL-MiniML
   6.298  
   6.299 -MINIML_NAMES = Generalize Instance Maybe MiniML Type W
   6.300 +HOL-MiniML: HOL $(LOG)/HOL-MiniML.gz
   6.301  
   6.302 -MINIML_FILES = MiniML/ROOT.ML \
   6.303 -	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   6.304 -
   6.305 -$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES)
   6.306 +$(LOG)/HOL-MiniML.gz: $(OUT)/HOL MiniML/Generalize.ML \
   6.307 +  MiniML/Generalize.thy MiniML/Instance.ML MiniML/Instance.thy \
   6.308 +  MiniML/Maybe.ML MiniML/Maybe.thy MiniML/MiniML.ML MiniML/MiniML.thy \
   6.309 +  MiniML/ROOT.ML MiniML/Type.ML MiniML/Type.thy MiniML/W.ML MiniML/W.thy
   6.310  	@$(ISATOOL) usedir $(OUT)/HOL MiniML
   6.311  
   6.312  
   6.313 -## Lexical analysis
   6.314 +## HOL-IOA
   6.315 +
   6.316 +HOL-IOA: HOL $(LOG)/HOL-IOA.gz
   6.317  
   6.318 -LEX_FILES = Auto AutoChopper Chopper Prefix
   6.319 +$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.ML IOA/Asig.thy IOA/IOA.ML \
   6.320 +  IOA/IOA.thy IOA/ROOT.ML IOA/Solve.ML IOA/Solve.thy
   6.321 +	@$(ISATOOL) usedir $(OUT)/HOL IOA
   6.322 +
   6.323 +
   6.324 +## HOL-AxClasses
   6.325 +
   6.326 +HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
   6.327  
   6.328 -LEX_FILES = Lex/ROOT.ML \
   6.329 -	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   6.330 +$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/ROOT.ML
   6.331 +	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   6.332 +
   6.333 +
   6.334 +## HOL-AxClasses-Group
   6.335  
   6.336 -$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES)
   6.337 -	@$(ISATOOL) usedir $(OUT)/HOL Lex
   6.338 +HOL-AxClasses-Group: HOL-AxClasses $(LOG)/HOL-AxClasses-Group.gz
   6.339 +
   6.340 +$(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \
   6.341 +  AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \
   6.342 +  AxClasses/Group/GroupDefs.thy AxClasses/Group/GroupInsts.thy \
   6.343 +  AxClasses/Group/Monoid.thy AxClasses/Group/MonoidGroupInsts.thy \
   6.344 +  AxClasses/Group/ROOT.ML AxClasses/Group/Sigs.thy
   6.345 +	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
   6.346  
   6.347  
   6.348 -## Axiomatic type classes examples
   6.349 -
   6.350 -AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \
   6.351 -	GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy
   6.352 +## HOL-AxClasses-Lattice
   6.353  
   6.354 -AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \
   6.355 -	LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \
   6.356 -	Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \
   6.357 -	Order.ML Order.thy ROOT.ML tools.ML
   6.358 +HOL-AxClasses-Lattice: HOL-AxClasses $(LOG)/HOL-AxClasses-Lattice.gz
   6.359  
   6.360 -AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \
   6.361 -	MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \
   6.362 -	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
   6.363 -	Xor.ML Xor.thy
   6.364 -
   6.365 -$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL
   6.366 -	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   6.367 -
   6.368 -$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
   6.369 -  $(AXC_GROUP_FILES:%=AxClasses/Group/%)
   6.370 -	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
   6.371 -
   6.372 -$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \
   6.373 -  $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%)
   6.374 +$(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \
   6.375 +  AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \
   6.376 +  AxClasses/Lattice/LatInsts.thy AxClasses/Lattice/LatMorph.ML \
   6.377 +  AxClasses/Lattice/LatMorph.thy AxClasses/Lattice/LatPreInsts.ML \
   6.378 +  AxClasses/Lattice/LatPreInsts.thy AxClasses/Lattice/Lattice.ML \
   6.379 +  AxClasses/Lattice/Lattice.thy AxClasses/Lattice/OrdDefs.ML \
   6.380 +  AxClasses/Lattice/OrdDefs.thy AxClasses/Lattice/OrdInsts.thy \
   6.381 +  AxClasses/Lattice/Order.ML AxClasses/Lattice/Order.thy \
   6.382 +  AxClasses/Lattice/ROOT.ML AxClasses/Lattice/tools.ML
   6.383  	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
   6.384  
   6.385 -$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \
   6.386 -  $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
   6.387 +
   6.388 +## HOL-AxClasses-Tutorial
   6.389 +
   6.390 +HOL-AxClasses-Tutorial: HOL-AxClasses $(LOG)/HOL-AxClasses-Tutorial.gz
   6.391 +
   6.392 +$(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \
   6.393 +  AxClasses/Tutorial/BoolGroupInsts.thy AxClasses/Tutorial/Group.ML \
   6.394 +  AxClasses/Tutorial/Group.thy AxClasses/Tutorial/Monoid.thy \
   6.395 +  AxClasses/Tutorial/MonoidGroupInsts.thy \
   6.396 +  AxClasses/Tutorial/ProdGroupInsts.thy AxClasses/Tutorial/Product.thy \
   6.397 +  AxClasses/Tutorial/ProductInsts.thy AxClasses/Tutorial/ROOT.ML \
   6.398 +  AxClasses/Tutorial/Semigroup.thy AxClasses/Tutorial/Semigroups.thy \
   6.399 +  AxClasses/Tutorial/Sigs.thy AxClasses/Tutorial/Xor.ML \
   6.400 +  AxClasses/Tutorial/Xor.thy
   6.401  	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
   6.402  
   6.403  
   6.404 -## Higher-order quotients and example fractionals
   6.405 +## HOL-Quot
   6.406 +
   6.407 +HOL-Quot: HOL $(LOG)/HOL-Quot.gz
   6.408  
   6.409 -QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
   6.410 -	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
   6.411 -	Quot/FRACT.thy Quot/FRACT.ML
   6.412 -
   6.413 -$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES)
   6.414 +$(LOG)/HOL-Quot.gz: $(OUT)/HOL Quot/FRACT.ML Quot/FRACT.thy \
   6.415 +  Quot/HQUOT.ML Quot/HQUOT.thy Quot/NPAIR.ML Quot/NPAIR.thy Quot/PER.ML \
   6.416 +  Quot/PER.thy Quot/PER0.ML Quot/PER0.thy Quot/ROOT.ML
   6.417  	@$(ISATOOL) usedir $(OUT)/HOL Quot
   6.418  
   6.419  
   6.420 -## Miscellaneous examples
   6.421 +## HOL-ex
   6.422  
   6.423 -EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
   6.424 +HOL-ex: HOL $(LOG)/HOL-ex.gz
   6.425  
   6.426 -EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   6.427 -	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   6.428 -
   6.429 -$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES)
   6.430 +$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/BT.ML ex/BT.thy ex/Fib.ML ex/Fib.thy \
   6.431 +  ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
   6.432 +  ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML ex/Primrec.thy \
   6.433 +  ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML \
   6.434 +  ex/Recdef.ML ex/Recdef.thy ex/String.ML ex/String.thy ex/cla.ML \
   6.435 +  ex/meson.ML ex/mesontest.ML ex/rel.ML ex/set.ML
   6.436  	@$(ISATOOL) usedir $(OUT)/HOL ex
   6.437  
   6.438  
   6.439 -## Full test
   6.440 +## TLA
   6.441 +
   6.442 +TLA: HOL $(OUT)/TLA
   6.443 +
   6.444 +$(OUT)/TLA: $(OUT)/HOL TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \
   6.445 +  TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \
   6.446 +  TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML
   6.447 +	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
   6.448 +
   6.449 +
   6.450 +## TLA-Inc
   6.451 +
   6.452 +TLA-Inc: TLA $(LOG)/TLA-Inc.gz
   6.453 +
   6.454 +$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy TLA/Inc/Inc.ML \
   6.455 +  TLA/Inc/Pcount.thy
   6.456 +	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
   6.457 +
   6.458 +
   6.459 +## TLA-Buffer
   6.460 +
   6.461 +TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
   6.462  
   6.463 -ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \
   6.464 -  $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \
   6.465 -  $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \
   6.466 -  $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
   6.467 -  $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
   6.468 -  $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
   6.469 -  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
   6.470 -  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz
   6.471 +$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \
   6.472 +  TLA/Buffer/Buffer.ML TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML
   6.473 +	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
   6.474 +
   6.475 +
   6.476 +## TLA-Memory
   6.477 +
   6.478 +TLA-Memory: TLA $(LOG)/TLA-Memory.gz
   6.479  
   6.480 -test: $(ALL_TARGETS)
   6.481 +$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MIParameters.thy \
   6.482 +  TLA/Memory/MIlive.ML TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML \
   6.483 +  TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.ML \
   6.484 +  TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.ML \
   6.485 +  TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.ML \
   6.486 +  TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.ML \
   6.487 +  TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.ML \
   6.488 +  TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.ML TLA/Memory/RPC.thy \
   6.489 +  TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.ML \
   6.490 +  TLA/Memory/RPCParameters.thy
   6.491 +	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
   6.492 +
   6.493 +
   6.494 +## clean
   6.495  
   6.496  clean:
   6.497 -	@rm -f $(ALL_TARGETS)
   6.498 -
   6.499 -
   6.500 -.PRECIOUS: $(OUT)/Pure $(OUT)/HOL
   6.501 +	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
   6.502 +	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
   6.503 +	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz \
   6.504 +	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
   6.505 +	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
   6.506 +	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
   6.507 +	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
   6.508 +	  $(LOG)/HOL-ex.gz $(OUT)/TLA $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz \
   6.509 +	  $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
     7.1 --- a/src/HOLCF/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     7.2 +++ b/src/HOLCF/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     7.3 @@ -4,43 +4,69 @@
     7.4  # IsaMakefile for HOLCF
     7.5  #
     7.6  
     7.7 -#### Base system
     7.8 +## targets
     7.9  
    7.10 +default: HOLCF
    7.11 +images: HOLCF IOA
    7.12 +test: HOLCF-IMP HOLCF-ex IOA-ABP IOA-NTP
    7.13 +all: images test
    7.14 +
    7.15 +
    7.16 +## global settings
    7.17 +
    7.18 +SRC = $(ISABELLE_HOME)/src
    7.19  OUT = $(ISABELLE_OUTPUT)
    7.20  LOG = $(OUT)/log
    7.21  
    7.22 -THYS = Porder.thy Porder0.thy Pcpo.thy \
    7.23 -       Fun1.thy Fun2.thy Fun3.thy \
    7.24 -       Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
    7.25 -       Cprod1.thy Cprod2.thy Cprod3.thy \
    7.26 -       Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
    7.27 -       Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
    7.28 -       Up1.thy Up2.thy Up3.thy Fix.thy \
    7.29 -       One.thy Tr.thy\
    7.30 -       Discrete0.thy Discrete1.thy Discrete.thy\
    7.31 -       Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
    7.32 +
    7.33 +## HOLCF
    7.34 +
    7.35 +HOLCF: HOL $(OUT)/HOLCF
    7.36 +
    7.37 +HOL:
    7.38 +	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    7.39  
    7.40 -ONLYTHYS = 
    7.41 -
    7.42 -FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \
    7.43 -	holcf_logic.ML cont_consts.ML \
    7.44 -        domain/library.ML  domain/syntax.ML   domain/axioms.ML \
    7.45 -        domain/theorems.ML domain/extender.ML domain/interface.ML
    7.46 -
    7.47 -$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
    7.48 +$(OUT)/HOLCF: $(OUT)/HOL Cfun1.ML Cfun1.thy Cfun2.ML Cfun2.thy \
    7.49 +  Cfun3.ML Cfun3.thy Cont.ML Cont.thy Cprod1.ML Cprod1.thy Cprod2.ML \
    7.50 +  Cprod2.thy Cprod3.ML Cprod3.thy Discrete.ML Discrete.thy Discrete0.ML \
    7.51 +  Discrete0.thy Discrete1.ML Discrete1.thy Fix.ML Fix.thy Fun1.ML \
    7.52 +  Fun1.thy Fun2.ML Fun2.thy Fun3.ML Fun3.thy HOLCF.ML HOLCF.thy Lift.ML \
    7.53 +  Lift.thy Lift1.ML Lift1.thy Lift2.ML Lift2.thy Lift3.ML Lift3.thy \
    7.54 +  One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy Porder0.ML \
    7.55 +  Porder0.thy ROOT.ML Sprod0.ML Sprod0.thy Sprod1.ML Sprod1.thy \
    7.56 +  Sprod2.ML Sprod2.thy Sprod3.ML Sprod3.thy Ssum0.ML Ssum0.thy Ssum1.ML \
    7.57 +  Ssum1.thy Ssum2.ML Ssum2.thy Ssum3.ML Ssum3.thy Tr.ML Tr.thy Up1.ML \
    7.58 +  Up1.thy Up2.ML Up2.thy Up3.ML Up3.thy adm.ML cont_consts.ML \
    7.59 +  domain/axioms.ML domain/extender.ML domain/interface.ML \
    7.60 +  domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML
    7.61  	@$(ISATOOL) usedir -b $(OUT)/HOL HOLCF
    7.62  
    7.63 -$(OUT)/HOL:
    7.64 -	@cd ../HOL; $(ISATOOL) make
    7.65 +
    7.66 +## HOLCF-IMP
    7.67  
    7.68 +HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
    7.69 +
    7.70 +$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/Denotational.ML \
    7.71 +  IMP/Denotational.thy IMP/ROOT.ML
    7.72 +	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
    7.73  
    7.74  
    7.75 -#### Tests and examples
    7.76 +## HOLCF-ex
    7.77 +
    7.78 +HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
    7.79  
    7.80 -## IOA meta theory and examples
    7.81 +$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \
    7.82 +  ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
    7.83 +  ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \
    7.84 +  ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML
    7.85 +	@$(ISATOOL) usedir $(OUT)/HOLCF ex
    7.86  
    7.87  
    7.88 -IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \
    7.89 +## IOA
    7.90 +
    7.91 +IOA: HOLCF $(OUT)/IOA
    7.92 +
    7.93 +$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \
    7.94    IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \
    7.95    IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \
    7.96    IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \
    7.97 @@ -54,72 +80,41 @@
    7.98    IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
    7.99    IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \
   7.100    IOA/meta_theory/Compositionality.thy
   7.101 -
   7.102 -
   7.103 -IOA_ABP_FILES = IOA/ABP/Abschannel.thy \
   7.104 -  IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \
   7.105 -  IOA/ABP/Action.thy IOA/ABP/Check.ML \
   7.106 -  IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
   7.107 -  IOA/ABP/Env.thy IOA/ABP/Impl.thy \
   7.108 -  IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \
   7.109 -  IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
   7.110 -  IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \
   7.111 -  IOA/ABP/Sender.thy IOA/ABP/Spec.thy 
   7.112 +	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
   7.113  
   7.114  
   7.115 -IOA_NTP_FILES = IOA/NTP/Abschannel.ML \
   7.116 -  IOA/NTP/Abschannel.thy IOA/NTP/Action.ML  \
   7.117 -  IOA/NTP/Action.thy IOA/NTP/Correctness.ML \
   7.118 -  IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
   7.119 -  IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \
   7.120 -  IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \
   7.121 -  IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
   7.122 -  IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \
   7.123 -  IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \
   7.124 -  IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
   7.125 -  IOA/NTP/Spec.thy 
   7.126 +## IOA-ABP
   7.127 +
   7.128 +IOA-ABP: IOA $(LOG)/IOA-ABP.gz
   7.129  
   7.130 - 
   7.131 -$(OUT)/IOA: $(OUT)/HOLCF $(IOA_FILES)
   7.132 -	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
   7.133 -
   7.134 -$(LOG)/IOA-ABP.gz: $(OUT)/IOA $(IOA_ABP_FILES)
   7.135 +$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \
   7.136 +  IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML IOA/ABP/Action.thy \
   7.137 +  IOA/ABP/Check.ML IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
   7.138 +  IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \
   7.139 +  IOA/ABP/Lemmas.ML IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
   7.140 +  IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
   7.141 +  IOA/ABP/Spec.thy
   7.142  	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
   7.143  
   7.144 -$(LOG)/IOA-NTP.gz: $(OUT)/IOA $(IOA_NTP_FILES)
   7.145 +
   7.146 +## IOA-NTP
   7.147 +
   7.148 +IOA-NTP: IOA $(LOG)/IOA-NTP.gz
   7.149 +
   7.150 +$(LOG)/IOA-NTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \
   7.151 +  IOA/NTP/Abschannel.thy IOA/NTP/Action.ML IOA/NTP/Action.thy \
   7.152 +  IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
   7.153 +  IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \
   7.154 +  IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
   7.155 +  IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.ML \
   7.156 +  IOA/NTP/Receiver.thy IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
   7.157 +  IOA/NTP/Spec.thy
   7.158  	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
   7.159  
   7.160  
   7.161 -## IMP
   7.162 -
   7.163 -IMP_THYS = IMP/Denotational.thy
   7.164 -IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
   7.165 -
   7.166 -$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF $(IMP_FILES)
   7.167 -	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
   7.168 -
   7.169 -
   7.170 -## Miscellaneous examples
   7.171 -
   7.172 -EX_THYS = ex/Dnat.thy ex/Stream.thy \
   7.173 -	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \
   7.174 -	  ex/Hoare.thy ex/Loop.thy
   7.175 -
   7.176 -EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
   7.177 -
   7.178 -$(LOG)/HOLCF-ex.gz: ex/ROOT.ML $(EX_FILES)
   7.179 -	@$(ISATOOL) usedir $(OUT)/HOLCF ex
   7.180 -
   7.181 -
   7.182 -## Full test
   7.183 -
   7.184 -ALL_TARGETS = $(OUT)/HOLCF $(OUT)/IOA $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
   7.185 -  $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz
   7.186 -
   7.187 -test: $(ALL_TARGETS)
   7.188 +## clean
   7.189  
   7.190  clean:
   7.191 -	@rm -f $(ALL_TARGETS)
   7.192 -
   7.193 -
   7.194 -.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
   7.195 +	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
   7.196 +	  $(LOG)/HOLCF-ex.gz $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \
   7.197 +	  $(LOG)/IOA-NTP.gz
     8.1 --- a/src/LCF/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     8.2 +++ b/src/LCF/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     8.3 @@ -4,24 +4,41 @@
     8.4  # IsaMakefile for LCF
     8.5  #
     8.6  
     8.7 +## targets
     8.8 +
     8.9 +default: LCF
    8.10 +images: LCF
    8.11 +test: LCF-ex
    8.12 +all: images test
    8.13 +
    8.14 +
    8.15 +## global settings
    8.16 +
    8.17 +SRC = $(ISABELLE_HOME)/src
    8.18  OUT = $(ISABELLE_OUTPUT)
    8.19  LOG = $(OUT)/log
    8.20  
    8.21 -FILES =	ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
    8.22 +
    8.23 +## LCF
    8.24 +
    8.25 +LCF: FOL $(OUT)/LCF
    8.26  
    8.27 -$(OUT)/LCF: $(OUT)/FOL $(FILES)
    8.28 +FOL:
    8.29 +	@cd $(SRC)/FOL; $(ISATOOL) make FOL
    8.30 +
    8.31 +$(OUT)/LCF: $(OUT)/FOL LCF.ML LCF.thy ROOT.ML fix.ML pair.ML simpdata.ML
    8.32  	@$(ISATOOL) usedir -b $(OUT)/FOL LCF
    8.33  
    8.34 -$(OUT)/FOL:
    8.35 -	@cd ../FOL; $(ISATOOL) make
    8.36 +
    8.37 +## LCF-ex
    8.38  
    8.39 -$(LOG)/LCF-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/LCF
    8.40 +LCF-ex: LCF $(LOG)/LCF-ex.gz
    8.41 +
    8.42 +$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/ROOT.ML ex/ex.ML
    8.43  	@$(ISATOOL) usedir $(OUT)/LCF ex
    8.44  
    8.45 -test: $(OUT)/LCF $(LOG)/LCF-ex.gz
    8.46 +
    8.47 +## clean
    8.48  
    8.49  clean:
    8.50 -	@rm -f $(OUT)/LCF $(LOG)/LCF-ex.gz
    8.51 -
    8.52 -
    8.53 -.PRECIOUS: $(OUT)/FOL $(OUT)/LCF
    8.54 +	@rm -f $(OUT)/LCF $(LOG)/LCF.gz $(LOG)/LCF-ex.gz
     9.1 --- a/src/Pure/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     9.2 +++ b/src/Pure/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     9.3 @@ -1,38 +1,51 @@
     9.4 -#
     9.5 -#  $Id$
     9.6  #
     9.7 -# IsaMakefile for Pure Isabelle
     9.8 +# $Id$
     9.9  #
    9.10 -# The Pure part is common to all systems. Object-logics (like FOL)
    9.11 -# are loaded on top of it.
    9.12 +# IsaMakefile for Pure
    9.13  #
    9.14  
    9.15 +## targets
    9.16 +
    9.17 +default: Pure
    9.18 +images: Pure
    9.19 +test:
    9.20 +all: images test
    9.21 +
    9.22 +
    9.23 +## global settings
    9.24 +
    9.25 +SRC = $(ISABELLE_HOME)/src
    9.26  OUT = $(ISABELLE_OUTPUT)
    9.27 +LOG = $(OUT)/log
    9.28 +
    9.29  
    9.30 -FILES = ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \
    9.31 -	ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \
    9.32 -	Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/pretty.ML \
    9.33 -	Syntax/printer.ML Syntax/symbol_font.ML Syntax/syn_ext.ML \
    9.34 -	Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \
    9.35 -	Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/file.ML \
    9.36 -	Thy/path.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML \
    9.37 -	Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \
    9.38 -	axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \
    9.39 -	goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \
    9.40 -	pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \
    9.41 -	sorts.ML table.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
    9.42 -	type.ML type_infer.ML unify.ML
    9.43 +## Pure
    9.44 +
    9.45 +Pure: $(OUT)/Pure
    9.46  
    9.47 -$(OUT)/Pure: $(FILES)
    9.48 +$(OUT)/Pure: ML-Systems/mlworks.ML ML-Systems/polyml.ML \
    9.49 +  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \
    9.50 +  Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
    9.51 +  Syntax/pretty.ML Syntax/printer.ML Syntax/symbol_font.ML \
    9.52 +  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \
    9.53 +  Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
    9.54 +  Thy/browser_info.ML Thy/context.ML Thy/file.ML Thy/path.ML \
    9.55 +  Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML \
    9.56 +  Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML \
    9.57 +  display.ML drule.ML envir.ML goals.ML install_pp.ML library.ML \
    9.58 +  logic.ML name_space.ML net.ML pattern.ML pure_thy.ML search.ML \
    9.59 +  section_utils.ML seq.ML sign.ML sorts.ML table.ML tactic.ML tctical.ML \
    9.60 +  term.ML theory.ML thm.ML type.ML type_infer.ML unify.ML
    9.61  	@./mk
    9.62  
    9.63 -RAW: $(FILES)
    9.64 +
    9.65 +## RAW
    9.66 +
    9.67 +RAW:
    9.68  	@./mk -r
    9.69  
    9.70 -test: $(OUT)/Pure
    9.71 +
    9.72 +## clean
    9.73  
    9.74  clean:
    9.75 -	@rm -f $(OUT)/Pure $(OUT)/RAW
    9.76 -
    9.77 -
    9.78 -.PRECIOUS: $(OUT)/Pure $(OUT)/RAW
    9.79 +	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz
    10.1 --- a/src/Sequents/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
    10.2 +++ b/src/Sequents/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
    10.3 @@ -4,32 +4,46 @@
    10.4  # IsaMakefile for Sequents
    10.5  #
    10.6  
    10.7 +## targets
    10.8 +
    10.9 +default: Sequents
   10.10 +images: Sequents
   10.11 +test: Sequents-ex
   10.12 +all: images test
   10.13 +
   10.14 +
   10.15 +## global settings
   10.16 +
   10.17 +SRC = $(ISABELLE_HOME)/src
   10.18  OUT = $(ISABELLE_OUTPUT)
   10.19  LOG = $(OUT)/log
   10.20  
   10.21 -NAMES = ILL LK S4 S43 T
   10.22 -FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
   10.23 +
   10.24 +## Sequents
   10.25 +
   10.26 +Sequents: Pure $(OUT)/Sequents
   10.27  
   10.28 -ILL_NAMES = ILL_predlog washing
   10.29 -EX_FILES = ex/ROOT.ML \
   10.30 -    ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \
   10.31 -    ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \
   10.32 -    ex/ILL/ILL_kleene_lemmas.ML \
   10.33 -    $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
   10.34 +Pure:
   10.35 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
   10.36  
   10.37 -$(OUT)/Sequents: $(OUT)/Pure $(FILES)
   10.38 +$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK.ML LK.thy ROOT.ML S4.ML \
   10.39 +  S4.thy S43.ML S43.thy Sequents.thy T.ML T.thy prover.ML
   10.40  	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
   10.41  
   10.42 -$(OUT)/Pure:
   10.43 -	@cd ../Pure; $(ISATOOL) make
   10.44 +
   10.45 +## Sequents-ex
   10.46 +
   10.47 +Sequents-ex: Sequents $(LOG)/Sequents-ex.gz
   10.48  
   10.49 -$(LOG)/Sequents-ex.gz: $(OUT)/Sequents $(EX_FILES)
   10.50 +$(LOG)/Sequents-ex.gz: $(OUT)/Sequents ex/ILL/ILL_kleene_lemmas.ML \
   10.51 +  ex/ILL/ILL_predlog.ML ex/ILL/ILL_predlog.thy ex/ILL/washing.ML \
   10.52 +  ex/ILL/washing.thy ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML \
   10.53 +  ex/LK/quant.ML ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML \
   10.54 +  ex/Modal/Tthms.ML ex/ROOT.ML
   10.55  	@$(ISATOOL) usedir $(OUT)/Sequents ex
   10.56  
   10.57 -test: $(OUT)/Sequents $(LOG)/Sequents-ex.gz
   10.58 +
   10.59 +## clean
   10.60  
   10.61  clean:
   10.62 -	@rm -f $(OUT)/Sequents $(LOG)/Sequents-ex.gz
   10.63 -
   10.64 -
   10.65 -.PRECIOUS: $(OUT)/Pure $(OUT)/Sequents
   10.66 +	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ex.gz
    11.1 --- a/src/ZF/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
    11.2 +++ b/src/ZF/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
    11.3 @@ -4,100 +4,118 @@
    11.4  # IsaMakefile for ZF
    11.5  #
    11.6  
    11.7 -#### Base system
    11.8 +## targets
    11.9  
   11.10 +default: ZF
   11.11 +images: ZF
   11.12 +test: ZF-IMP ZF-Coind ZF-AC ZF-Resid ZF-ex
   11.13 +all: images test
   11.14 +
   11.15 +
   11.16 +## global settings
   11.17 +
   11.18 +SRC = $(ISABELLE_HOME)/src
   11.19  OUT = $(ISABELLE_OUTPUT)
   11.20  LOG = $(OUT)/log
   11.21  
   11.22 -NAMES = ZF upair subset pair domrange \
   11.23 -	func AC equalities Bool \
   11.24 -	Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
   11.25 -	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
   11.26 -	WF Order Ordinal Epsilon Arith Univ \
   11.27 -	QUniv Datatype OrderArith OrderType \
   11.28 -	Cardinal CardinalArith Cardinal_AC InfDatatype \
   11.29 -	Zorn Nat Finite List
   11.30 +
   11.31 +## ZF
   11.32 +
   11.33 +ZF: FOL $(OUT)/ZF
   11.34 +
   11.35 +FOL:
   11.36 +	@cd $(SRC)/FOL; $(ISATOOL) make FOL
   11.37  
   11.38 -FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \
   11.39 -	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
   11.40 -
   11.41 -$(OUT)/ZF: $(OUT)/FOL $(FILES)
   11.42 +$(OUT)/ZF: $(OUT)/FOL $(SRC)/Pure/section_utils.ML AC.ML AC.thy \
   11.43 +  Arith.ML Arith.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \
   11.44 +  CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy \
   11.45 +  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy EquivClass.ML \
   11.46 +  EquivClass.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy \
   11.47 +  Inductive.ML Inductive.thy InfDatatype.ML InfDatatype.thy List.ML \
   11.48 +  List.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \
   11.49 +  OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \
   11.50 +  Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML \
   11.51 +  Rel.thy Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy WF.ML \
   11.52 +  WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy add_ind_def.ML add_ind_def.thy \
   11.53 +  cartprod.ML cartprod.thy constructor.ML constructor.thy domrange.ML \
   11.54 +  domrange.thy equalities.ML equalities.thy func.ML func.thy \
   11.55 +  ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
   11.56 +  intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
   11.57 +  subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy
   11.58  	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
   11.59  
   11.60 -$(OUT)/FOL:
   11.61 -	@cd ../FOL; $(ISATOOL) make
   11.62  
   11.63 -
   11.64 -
   11.65 -#### Tests and examples
   11.66 +## ZF-IMP
   11.67  
   11.68 -## IMP-semantics example
   11.69 +ZF-IMP: ZF $(LOG)/ZF-IMP.gz
   11.70  
   11.71 -IMP_NAMES = Com Denotation Equiv
   11.72 -IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
   11.73 -
   11.74 -$(LOG)/ZF-IMP.gz: $(OUT)/ZF $(IMP_FILES)
   11.75 +$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
   11.76 +  IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML
   11.77  	@$(ISATOOL) usedir $(OUT)/ZF IMP
   11.78  
   11.79  
   11.80 -## Coinduction example
   11.81 +## ZF-Coind
   11.82  
   11.83 -COIND_NAMES = ECR MT Map Static Types Values
   11.84 +ZF-Coind: ZF $(LOG)/ZF-Coind.gz
   11.85  
   11.86 -COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \
   11.87 -	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
   11.88 -
   11.89 -$(LOG)/ZF-Coind.gz: $(OUT)/ZF $(COIND_FILES)
   11.90 +$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
   11.91 +  Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \
   11.92 +  Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \
   11.93 +  Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \
   11.94 +  Coind/Values.thy
   11.95  	@$(ISATOOL) usedir $(OUT)/ZF Coind
   11.96  
   11.97  
   11.98 -## AC examples
   11.99 +## ZF-AC
  11.100  
  11.101 -AC_NAMES = AC_Equiv Cardinal_aux \
  11.102 -	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
  11.103 -	   DC DC_lemmas HH Hartog WO1_AC \
  11.104 -	   WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun
  11.105 +ZF-AC: ZF $(LOG)/ZF-AC.gz
  11.106  
  11.107 -AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
  11.108 -	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
  11.109 -	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
  11.110 -	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
  11.111 -
  11.112 -$(LOG)/ZF-AC.gz: $(OUT)/ZF $(AC_FILES)
  11.113 +$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/AC0_AC1.ML AC/AC10_AC15.ML \
  11.114 +  AC/AC15_WO6.ML AC/AC15_WO6.thy AC/AC16_WO4.ML AC/AC16_WO4.thy \
  11.115 +  AC/AC16_lemmas.ML AC/AC16_lemmas.thy AC/AC17_AC1.ML AC/AC17_AC1.thy \
  11.116 +  AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_AC17.ML AC/AC1_WO2.ML \
  11.117 +  AC/AC1_WO2.thy AC/AC2_AC6.ML AC/AC7_AC9.ML AC/AC_Equiv.ML \
  11.118 +  AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \
  11.119 +  AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \
  11.120 +  AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \
  11.121 +  AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML AC/WO2_AC16.ML \
  11.122 +  AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \
  11.123 +  AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy
  11.124  	@$(ISATOOL) usedir $(OUT)/ZF AC
  11.125  
  11.126  
  11.127 -## Residuals example
  11.128 +## ZF-Resid
  11.129 +
  11.130 +ZF-Resid: ZF $(LOG)/ZF-Resid.gz
  11.131  
  11.132 -RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
  11.133 -	      Cube Residuals Terms
  11.134 -
  11.135 -RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
  11.136 -
  11.137 -$(LOG)/ZF-Resid.gz: $(OUT)/ZF $(RESID_FILES)
  11.138 +$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \
  11.139 +  Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
  11.140 +  Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
  11.141 +  Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
  11.142 +  Resid/SubUnion.ML Resid/SubUnion.thy Resid/Substitution.ML \
  11.143 +  Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
  11.144  	@$(ISATOOL) usedir $(OUT)/ZF Resid
  11.145  
  11.146  
  11.147 -## Miscellaneous examples
  11.148 +## ZF-ex
  11.149 +
  11.150 +ZF-ex: ZF $(LOG)/ZF-ex.gz
  11.151  
  11.152 -EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
  11.153 -	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit
  11.154 -
  11.155 -EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
  11.156 -
  11.157 -$(LOG)/ZF-ex.gz: $(OUT)/ZF $(EX_FILES)
  11.158 +$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \
  11.159 +  ex/Bin.ML ex/Bin.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
  11.160 +  ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \
  11.161 +  ex/Enum.thy ex/Integ.ML ex/Integ.thy ex/LList.ML ex/LList.thy \
  11.162 +  ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
  11.163 +  ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
  11.164 +  ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
  11.165 +  ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
  11.166 +  ex/Term.ML ex/Term.thy ex/misc.ML ex/twos_compl.ML ex/twos_compl.thy
  11.167  	@$(ISATOOL) usedir $(OUT)/ZF ex
  11.168  
  11.169  
  11.170 -## Full test
  11.171 -
  11.172 -ALL_TARGETS = $(OUT)/ZF $(LOG)/ZF-IMP.gz $(LOG)/ZF-Coind.gz \
  11.173 -  $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz $(LOG)/ZF-ex.gz
  11.174 -
  11.175 -test: $(ALL_TARGETS)
  11.176 +## clean
  11.177  
  11.178  clean:
  11.179 -	@rm -f $(ALL_TARGETS)
  11.180 -
  11.181 -
  11.182 -.PRECIOUS: $(OUT)/FOL $(OUT)/ZF
  11.183 +	@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-IMP.gz \
  11.184 +	  $(LOG)/ZF-Coind.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz \
  11.185 +	  $(LOG)/ZF-ex.gz