equal
deleted
inserted
replaced
|
1 # |
|
2 # $Id$ |
|
3 # |
|
4 # IsaMakefile for Pure Isabelle |
|
5 # |
|
6 # The Pure part is common to all systems. Object-logics (like FOL) |
|
7 # are loaded on top of it. |
|
8 # |
|
9 # How to build: |
|
10 # (1) put the Isabelle bin dir into your PATH (try 'which isabelle') |
|
11 # (2) make sure Isabelle's etc/settings are appropriate (ML system etc.) |
|
12 # (3) cd here and run 'isatool make' |
|
13 # |
|
14 |
|
15 OUT = $(ISABELLE_OUTPUT_DIR) |
|
16 |
|
17 FILES = ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \ |
|
18 ML-Systems/smlnj-1.07.ML ML-Systems/smlnj-1.09.ML ROOT.ML \ |
|
19 Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML \ |
|
20 Syntax/parser.ML Syntax/pretty.ML Syntax/printer.ML \ |
|
21 Syntax/symbol_font.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ |
|
22 Syntax/syntax.ML Syntax/type_ext.ML Thy/ROOT.ML Thy/symbol_input.ML \ |
|
23 Thy/thm_database.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \ |
|
24 Thy/thy_syn.ML axclass.ML basis.ML deriv.ML display.ML drule.ML \ |
|
25 envir.ML goals.ML install_pp.ML library.ML logic.ML net.ML pattern.ML \ |
|
26 search.ML section_utils.ML sequence.ML sign.ML symtab.ML tactic.ML \ |
|
27 tctical.ML term.ML theory.ML thm.ML type.ML unify.ML \ |
|
28 ../Provers/simplifier.ML |
|
29 |
|
30 $(OUT)/Pure: $(FILES) |
|
31 @./mk |
|
32 |
|
33 test: $(OUT)/Pure |
|
34 |
|
35 .PRECIOUS: $(OUT)/Pure |