author  wenzelm 
Fri, 21 Oct 2005 18:14:42 +0200  
changeset 17962  d4d2c854600b 
parent 17927  4b42562ec171 
child 18059  ce6cff74931b 
permissions  rwrr 
2431  1 
# 
4518  2 
# $Id$ 
2431  3 
# 
4518  4 
# IsaMakefile for Pure 
2431  5 
# 
6 

4518  7 
## targets 
8 

9 
default: Pure 

10 
images: Pure 

11 
test: 

12 
all: images test 

13 

14 

15 
## global settings 

16 

17 
SRC = $(ISABELLE_HOME)/src 

3118  18 
OUT = $(ISABELLE_OUTPUT) 
4518  19 
LOG = $(OUT)/log 
20 

2431  21 

4518  22 
## Pure 
23 

17802
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
17338
diff
changeset

24 
Pure: $(OUT)/Pure$(ML_SUFFIX) 
2431  25 

17802
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
17338
diff
changeset

26 
$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \ 
17154  27 
General/buffer.ML \ 
28 
General/file.ML General/graph.ML General/heap.ML General/history.ML \ 

17848  29 
General/name_space.ML \ 
17154  30 
General/ord_list.ML General/output.ML General/path.ML \ 
31 
General/position.ML General/pretty.ML General/scan.ML General/seq.ML \ 

17848  32 
General/rat.ML \ 
33 
General/source.ML General/stack.ML General/symbol.ML \ 

34 
General/table.ML General/url.ML General/xml.ML \ 

35 
IsaPlanner/focus_term_lib.ML \ 

17154  36 
IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML \ 
37 
IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML \ 

38 
IsaPlanner/upterm_lib.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \ 

39 
Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \ 

40 
Isar/constdefs.ML Isar/context_rules.ML Isar/find_theorems.ML \ 

41 
Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML \ 

42 
Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML Isar/method.ML \ 

43 
Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ 

44 
Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ 

17848  45 
Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \ 
46 
Isar/proof_display.ML \ 

17154  47 
Isar/proof_history.ML Isar/rule_cases.ML Isar/session.ML \ 
48 
Isar/skip_proof.ML Isar/term_style.ML Isar/thy_header.ML \ 

49 
Isar/toplevel.ML MLSystems/cputimerbasis.ML \ 

17802
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
17338
diff
changeset

50 
MLSystems/cputimergc.ML MLSystems/poplogml.ML \ 
17154  51 
MLSystems/polymltimelimit.ML MLSystems/polyml.ML \ 
52 
MLSystems/polymlposix.ML MLSystems/smlnjbasiscompat.ML \ 

53 
MLSystems/smlnjcompiler.ML MLSystems/smlnjptreql.ML \ 

54 
MLSystems/smlnjppnew.ML MLSystems/smlnjppold.ML \ 

55 
MLSystems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \ 

56 
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ 

57 
Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \ 

58 
Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \ 

59 
Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ 

60 
Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/present.ML \ 

61 
Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML \ 

17927
4b42562ec171
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
wenzelm
parents:
17848
diff
changeset

62 
axclass.ML Tools/am_compiler.ML Tools/am_interpreter.ML \ 
4b42562ec171
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
wenzelm
parents:
17848
diff
changeset

63 
Tools/am_util.ML Tools/compute.ML Tools/ROOT.ML codegen.ML compress.ML\ 
17962  64 
context.ML display.ML drule.ML envir.ML fact_index.ML goal.ML \ 
17154  65 
goals.ML install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML \ 
66 
pattern.ML proof_general.ML proofterm.ML pure_thy.ML search.ML \ 

67 
sign.ML simplifier.ML sorts.ML tactic.ML tctical.ML term.ML defs.ML \ 

16532
e248ffc956c7
removed Pure/Isar/proof_data.ML, Pure/General/object.ML;
wenzelm
parents:
16528
diff
changeset

68 
theory.ML thm.ML type.ML type_infer.ML unify.ML 
2431  69 
@./mk 
70 

4518  71 

10102  72 
## special targets 
73 

74 
Purecopied: 

75 
@./mk C 

4518  76 

77 
RAW: 

3774  78 
@./mk r 
79 

10102  80 
RAWcopied: 
81 
@./mk Cr 

82 

4518  83 

84 
## clean 

4441  85 

86 
clean: 

17802
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
17338
diff
changeset

87 
@rm f $(OUT)/Pure$(ML_SUFFIX) $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz 