| author | nipkow | 
| Wed, 02 Feb 2005 10:16:33 +0100 | |
| changeset 15485 | e93a3badc2bc | 
| parent 11260 | b736de4cb913 | 
| child 17252 | e352f65d5893 | 
| permissions | -rw-r--r-- | 
| 2487 | 1 | # | 
| 2 | # $Id$ | |
| 3 | # | |
| 4 | # IsaMakefile for Cube | |
| 5 | # | |
| 6 | ||
| 4518 | 7 | ## targets | 
| 8 | ||
| 9 | default: Cube | |
| 10 | images: Cube | |
| 11 | test: Cube-ex | |
| 12 | all: images test | |
| 13 | ||
| 14 | ||
| 15 | ## global settings | |
| 16 | ||
| 17 | SRC = $(ISABELLE_HOME)/src | |
| 3118 | 18 | OUT = $(ISABELLE_OUTPUT) | 
| 4447 | 19 | LOG = $(OUT)/log | 
| 20 | ||
| 4518 | 21 | |
| 22 | ## Cube | |
| 23 | ||
| 24 | Cube: Pure $(OUT)/Cube | |
| 2487 | 25 | |
| 4518 | 26 | Pure: | 
| 27 | @cd $(SRC)/Pure; $(ISATOOL) make Pure | |
| 28 | ||
| 4583 | 29 | $(OUT)/Cube: $(OUT)/Pure Base.ML Base.thy CC.ML CC.thy Cube.thy L2.ML \ | 
| 11260 
b736de4cb913
renaming of theory LOmega to lomega2 in order to prevent a possible
 paulson parents: 
4583diff
changeset | 30 | L2.thy Lomega2.ML Lomega2.thy LP.ML LP.thy LP2.ML LP2.thy LPomega.ML \ | 
| 4583 | 31 | LPomega.thy Lomega.ML Lomega.thy ROOT.ML | 
| 2819 | 32 | @$(ISATOOL) usedir -b $(OUT)/Pure Cube | 
| 2487 | 33 | |
| 4518 | 34 | |
| 35 | ## Cube-ex | |
| 2487 | 36 | |
| 4518 | 37 | Cube-ex: Cube $(LOG)/Cube-ex.gz | 
| 38 | ||
| 4583 | 39 | $(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ex.thy ex/ROOT.ML | 
| 2819 | 40 | @$(ISATOOL) usedir $(OUT)/Cube ex | 
| 2487 | 41 | |
| 4518 | 42 | |
| 43 | ## clean | |
| 4447 | 44 | |
| 45 | clean: | |
| 4518 | 46 | @rm -f $(OUT)/Cube $(LOG)/Cube.gz $(LOG)/Cube-ex.gz |