added AxClasses test;
authorwenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545d10abc8c11fb
parent 2544 67b444ca0e4f
child 2546 866957616069
added AxClasses test;
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Thu Jan 23 14:05:42 1997 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jan 23 14:19:16 1997 +0100
     1.3 @@ -156,6 +156,33 @@
     1.4  	@$(ISATOOL) testdir $(OUT)/HOL Lex
     1.5  
     1.6  
     1.7 +## Axiomatic type classes examples
     1.8 +
     1.9 +AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \
    1.10 +	GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy
    1.11 +
    1.12 +AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \
    1.13 +	LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \
    1.14 +	Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \
    1.15 +	Order.ML Order.thy ROOT.ML tools.ML
    1.16 +
    1.17 +AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \
    1.18 +	MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \
    1.19 +	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
    1.20 +	Xor.ML Xor.thy
    1.21 +
    1.22 +AXCLASSES_FILES = AxClasses/ROOT.ML \
    1.23 +	$(AXC_GROUP_FILES:%=AxClasses/Group/%) \
    1.24 +	$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
    1.25 +	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
    1.26 +
    1.27 +AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
    1.28 +	@$(ISATOOL) testdir $(OUT)/HOL AxClasses
    1.29 +	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Group
    1.30 +	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Lattice
    1.31 +	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Tutorial
    1.32 +
    1.33 +
    1.34  ## Miscellaneous examples
    1.35  
    1.36  EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
    1.37 @@ -170,7 +197,8 @@
    1.38  
    1.39  ## Full test
    1.40  
    1.41 -test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA ex
    1.42 +test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML \
    1.43 +	IOA AxClasses ex
    1.44  	echo 'Test examples ran successfully' > test
    1.45  
    1.46