Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IsaMakefile
author oheimb
Mon, 24 Feb 1997 16:12:24 +0100
changeset 2679 3eac428cdd1b
parent 2640 ee4dfce170a0
child 2797 54ca927b831b
permissions -rw-r--r--
removed explicit_domains/, which is now covered by ex/

#
# $Id$
#
# IsaMakefile for HOLCF
#

#### Base system

OUT = $(ISABELLE_OUTPUT_DIR)

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 ccc1.thy \
       One.thy Tr.thy\
       Lift1.thy Lift2.thy Lift3.thy HOLCF.thy 

ONLYTHYS = Lift.thy

FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)

$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
	@chmod -w $@

$(OUT)/HOL:
	@cd ../HOL; $(ISATOOL) make



#### Tests and examples

## Miscellaneous examples

EX_THYS = ex/Classlib.thy ex/Witness.thy\
	  ex/Dnat.thy ex/Dlist.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)

test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
	@$(ISATOOL) testdir $(OUT)/HOLCF ex

.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
isabelle