author  wenzelm 
Wed, 26 Jul 2006 00:44:44 +0200  
changeset 20207  4c57e850e8d5 
parent 20075  a7e183bfebef 
child 20225  4b8e42490e58 
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 

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

28 
General/history.ML General/name_mangler.ML General/name_space.ML \ 

29 
General/ord_list.ML General/output.ML General/path.ML \ 

30 
General/position.ML General/pretty.ML General/rat.ML General/scan.ML \ 

31 
General/seq.ML General/source.ML General/stack.ML General/symbol.ML \ 

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

33 
Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \ 

34 
Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML \ 

35 
Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML \ 

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

37 
Isar/isar_syn.ML Isar/isar_thy.ML Isar/local_defs.ML \ 

38 
Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ 

39 
Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ 

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

41 
Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \ 

42 
Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML \ 

43 
Isar/session.ML Isar/skip_proof.ML Isar/specification.ML \ 

44 
Isar/term_style.ML Isar/thy_header.ML Isar/toplevel.ML \ 

45 
MLSystems/cputimerbasis.ML MLSystems/cputimergc.ML \ 

46 
MLSystems/polyml4.1.4patch.ML MLSystems/polyml4.2.0.ML \ 

47 
MLSystems/polymlinterrupttimeout.ML MLSystems/polymlposix.ML \ 

48 
MLSystems/polyml.ML MLSystems/poplogml.ML \ 

49 
MLSystems/smlnjbasiscompat.ML MLSystems/smlnjcompiler.ML \ 

50 
MLSystems/smlnjinterrupttimeout.ML MLSystems/smlnjppnew.ML \ 

51 
MLSystems/smlnjppold.ML MLSystems/smlnjptreql.ML \ 

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

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

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

55 
Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \ 

56 
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \ 

57 
Thy/latex.ML Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML \ 

58 
Thy/thy_info.ML Thy/thy_load.ML Tools/ROOT.ML Tools/am_compiler.ML \ 

59 
Tools/am_interpreter.ML Tools/am_util.ML Tools/class_package.ML \ 

60 
Tools/codegen_package.ML Tools/codegen_serializer.ML \ 

19885  61 
Tools/codegen_theorems.ML Tools/codegen_simtype.ML \ 
62 
Tools/codegen_thingol.ML Tools/compute.ML \ 

19807  63 
Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML \ 
64 
axclass.ML codegen.ML compress.ML conjunction.ML consts.ML context.ML defs.ML \ 

19415  65 
display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML \ 
20075  66 
library.ML logic.ML meta_simplifier.ML name.ML net.ML old_goals.ML pattern.ML \ 
19415  67 
proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML \ 
20207  68 
simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML theory.ML \ 
69 
thm.ML type.ML type_infer.ML variable.ML unify.ML 

2431  70 
@./mk 
71 

4518  72 

10102  73 
## special targets 
74 

75 
Purecopied: 

76 
@./mk C 

4518  77 

78 
RAW: 

3774  79 
@./mk r 
80 

10102  81 
RAWcopied: 
82 
@./mk Cr 

83 

4518  84 

85 
## clean 

4441  86 

87 
clean: 

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

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