src/Pure/IsaMakefile
author nipkow
Fri Nov 28 07:35:10 1997 +0100 (1997-11-28)
changeset 4318 9b672ea2dfe7
parent 4270 957c887b89b5
child 4337 062cdcb04b08
permissions -rw-r--r--
Fixed the definition of `termord': is now antisymmetric.
wenzelm@2431
     1
#
wenzelm@2431
     2
#  $Id$
wenzelm@2431
     3
#
wenzelm@2431
     4
# IsaMakefile for Pure Isabelle
wenzelm@2431
     5
#
wenzelm@2431
     6
# The Pure part is common to all systems. Object-logics (like FOL)
wenzelm@2431
     7
# are loaded on top of it.
wenzelm@2431
     8
#
wenzelm@2431
     9
wenzelm@3118
    10
OUT = $(ISABELLE_OUTPUT)
wenzelm@2431
    11
wenzelm@4208
    12
FILES = ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \
wenzelm@4208
    13
	ML-Systems/smlnj-1.09.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \
wenzelm@4208
    14
	Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/pretty.ML \
wenzelm@4208
    15
	Syntax/printer.ML Syntax/symbol_font.ML Syntax/syn_ext.ML \
wenzelm@4208
    16
	Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \
wenzelm@4208
    17
	Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/file.ML \
wenzelm@4208
    18
	Thy/path.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML \
wenzelm@4208
    19
	Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \
wenzelm@4256
    20
	axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \
wenzelm@4208
    21
	goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \
wenzelm@4270
    22
	pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \
wenzelm@4208
    23
	sorts.ML symtab.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
wenzelm@4208
    24
	type.ML type_infer.ML unify.ML
wenzelm@2431
    25
wenzelm@3869
    26
$(OUT)/Pure: $(FILES)
wenzelm@2431
    27
	@./mk
wenzelm@2431
    28
wenzelm@3926
    29
RAW: $(FILES)
wenzelm@3774
    30
	@./mk -r
wenzelm@3774
    31
wenzelm@3774
    32
test: Pure
wenzelm@2431
    33
wenzelm@3869
    34
.PRECIOUS: $(OUT)/Pure $(OUT)/RAW