src/HOL/IsaMakefile
changeset 29748 2ff24d87fad1
parent 29708 e40b70d38909
child 30101 5c6efec476ae
     1.1 --- a/src/HOL/IsaMakefile	Sun Feb 15 21:26:25 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Feb 16 12:27:30 2009 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4    HOL-Library \
     1.5    HOL-ex \
     1.6    HOL-Auth \
     1.7 -  HOL-AxClasses \
     1.8    HOL-Bali \
     1.9    HOL-Extraction \
    1.10    HOL-HahnBanach \
    1.11 @@ -770,15 +769,6 @@
    1.12  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
    1.13  
    1.14  
    1.15 -## HOL-AxClasses
    1.16 -
    1.17 -HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
    1.18 -
    1.19 -$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
    1.20 -  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
    1.21 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
    1.22 -
    1.23 -
    1.24  ## HOL-Lattice
    1.25  
    1.26  HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
    1.27 @@ -1045,22 +1035,22 @@
    1.28  ## clean
    1.29  
    1.30  clean:
    1.31 -	@rm -f  $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
    1.32 -		$(LOG)/HOL.gz $(LOG)/TLA.gz \
    1.33 -		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
    1.34 -		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
    1.35 -		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
    1.36 -		$(LOG)/HOL-HoareParallel.gz \
    1.37 -		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.38 -		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.39 -		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.40 -                $(LOG)/HOL-Bali.gz \
    1.41 -		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
    1.42 -                $(LOG)/HOL-Nominal-Examples.gz \
    1.43 -		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
    1.44 -		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
    1.45 -		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
    1.46 -                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
    1.47 -		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz \
    1.48 -                $(OUT)/HOL-Word $(LOG)/HOL-Word.gz $(LOG)/HOL-Word-Examples.gz \
    1.49 -                $(OUT)/HOL-NSA $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
    1.50 +	@rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL		\
    1.51 +		$(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz		\
    1.52 +		$(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz		\
    1.53 +		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
    1.54 +		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
    1.55 +		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\
    1.56 +		$(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz		\
    1.57 +		$(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz		\
    1.58 +		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
    1.59 +		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
    1.60 +		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
    1.61 +		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
    1.62 +		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
    1.63 +		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz	\
    1.64 +		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz			\
    1.65 +		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
    1.66 +		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
    1.67 +		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
    1.68 +		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz