src/HOL/IsaMakefile
author paulson
Tue, 01 Jul 1997 17:42:36 +0200
changeset 3482 ef918a90f9bf
parent 3417 58ccb80eb50a
child 3505 1cb4ea47d967
permissions -rw-r--r--
New theory TLS
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     1
#
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     2
# $Id$
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     3
#
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     4
# IsaMakefile for HOL
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     5
#
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     6
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     7
#### Base system
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     8
3118
24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
wenzelm
parents: 3079
diff changeset
     9
OUT = $(ISABELLE_OUTPUT)
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    10
3195
dcb458d38724 Preliminary TFL versions
paulson
parents: 3125
diff changeset
    11
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
3025
ab6bcbd130a1 Added NatDef
nipkow
parents: 2982
diff changeset
    12
	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents: 3369
diff changeset
    13
	Divides Power Sexp Univ List RelPow Option
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    14
3232
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    15
PROVERS = hypsubst.ML classical.ML blast.ML \
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    16
	simplifier.ML splitter.ML nat_transitive.ML 
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    17
3354
3dac85693547 Removal of mask.sig and mask.sml
paulson
parents: 3337
diff changeset
    18
TFL   = dcterm.sml post.sml rules.new.sml rules.sig \
3232
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    19
	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    20
	usyntax.sig usyntax.sml utils.sig utils.sml
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    21
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    22
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    23
	ind_syntax.ML cladata.ML simpdata.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    24
	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
3232
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    25
	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    26
	$(PROVERS:%=../Provers/%)
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    27
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    28
$(OUT)/HOL: $(OUT)/Pure $(FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
    29
	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    30
	@chmod -w $@
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    31
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    32
$(OUT)/Pure:
2473
3eb12c85846c minor tuning;
wenzelm
parents: 2448
diff changeset
    33
	@cd ../Pure; $(ISATOOL) make
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    34
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    35
2473
3eb12c85846c minor tuning;
wenzelm
parents: 2448
diff changeset
    36
#### Tests and examples
3eb12c85846c minor tuning;
wenzelm
parents: 2448
diff changeset
    37
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    38
## Inductive definitions: simple examples
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    39
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    40
INDUCT_FILES =  Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    41
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    42
INDUCT_FILES = Induct/ROOT.ML \
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    43
	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    44
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    45
Induct:	$(OUT)/HOL $(INDUCT_FILES)
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    46
	@$(ISATOOL) usedir $(OUT)/HOL Induct
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    47
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
    48
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    49
## IMP-semantics example
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    50
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    51
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    52
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    53
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    54
IMP:	$(OUT)/HOL $(IMP_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
    55
	@$(ISATOOL) usedir $(OUT)/HOL IMP
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    56
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    57
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    58
## Hoare logic
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    59
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    60
Hoare_NAMES = Hoare Arith2 Examples
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    61
Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    62
	      $(Hoare_NAMES:%=Hoare/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    63
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    64
Hoare:	$(OUT)/HOL $(Hoare_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
    65
	@$(ISATOOL) usedir $(OUT)/HOL Hoare
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    66
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    67
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    68
## The integers in HOL
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    69
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    70
INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    71
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    72
INTEG_FILES = Integ/ROOT.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    73
	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    74
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    75
Integ:	$(OUT)/HOL $(INTEG_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
    76
	@$(ISATOOL) usedir $(OUT)/HOL Integ
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    77
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    78
3079
2ea678d3523f removed (most of) IOA (see HOLCF/IOA);
mueller
parents: 3025
diff changeset
    79
## I/O Automata (meta theory only)
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    80
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    81
3079
2ea678d3523f removed (most of) IOA (see HOLCF/IOA);
mueller
parents: 3025
diff changeset
    82
IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
2ea678d3523f removed (most of) IOA (see HOLCF/IOA);
mueller
parents: 3025
diff changeset
    83
  IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    84
3079
2ea678d3523f removed (most of) IOA (see HOLCF/IOA);
mueller
parents: 3025
diff changeset
    85
IOA: $(OUT)/HOL $(IOA_FILES)
2ea678d3523f removed (most of) IOA (see HOLCF/IOA);
mueller
parents: 3025
diff changeset
    86
	@$(ISATOOL) usedir $(OUT)/HOL IOA
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    87
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    88
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    89
## Authentication & Security Protocols
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    90
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    91
Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
3482
ef918a90f9bf New theory TLS
paulson
parents: 3417
diff changeset
    92
	     Recur WooLam Yahalom Yahalom2 \
ef918a90f9bf New theory TLS
paulson
parents: 3417
diff changeset
    93
	     Public NS_Public_Bad NS_Public TLS
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    94
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    95
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    96
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    97
Auth:	$(OUT)/HOL $(AUTH_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
    98
	@$(ISATOOL) usedir $(OUT)/HOL Auth
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    99
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   100
3218
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   101
## Modelchecker invocation
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   102
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   103
MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   104
  Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   105
  Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   106
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   107
Modelcheck: $(OUT)/HOL $(MC_FILES)
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   108
	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   109
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   110
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   111
## Properties of substitutions
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   112
3195
dcb458d38724 Preliminary TFL versions
paulson
parents: 3125
diff changeset
   113
SUBST_NAMES = AList Subst Unifier UTerm Unify
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   114
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   115
SUBST_FILES = Subst/ROOT.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   116
	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   117
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   118
Subst:	$(OUT)/HOL $(SUBST_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   119
	@$(ISATOOL) usedir $(OUT)/HOL Subst
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   120
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   121
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   122
## Confluence of Lambda-calculus
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   123
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   124
LAMBDA_NAMES = Lambda ParRed Commutation Eta
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   125
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   126
LAMBDA_FILES = Lambda/ROOT.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   127
	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   128
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   129
Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   130
	@$(ISATOOL) usedir $(OUT)/HOL Lambda
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   131
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   132
2527
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   133
## Type inference without let
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   134
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   135
W0_NAMES = I Maybe MiniML Type W
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   136
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   137
W0_FILES = W0/ROOT.ML \
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   138
	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   139
2527
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   140
W0: $(OUT)/HOL $(W0_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   141
	@$(ISATOOL) usedir $(OUT)/HOL W0
2527
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   142
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   143
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   144
## Type inference with let
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   145
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   146
MINIML_NAMES = Generalize Instance Maybe MiniML Type W
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   147
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   148
MINIML_FILES = MiniML/ROOT.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   149
	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   150
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   151
MiniML: $(OUT)/HOL $(MINIML_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   152
	@$(ISATOOL) usedir $(OUT)/HOL MiniML
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   153
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   154
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   155
## Lexical analysis
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   156
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   157
LEX_FILES = Auto AutoChopper Chopper Prefix
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   158
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   159
LEX_FILES = Lex/ROOT.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   160
	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   161
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   162
Lex:	$(OUT)/HOL $(LEX_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   163
	@$(ISATOOL) usedir $(OUT)/HOL Lex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   164
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   165
2545
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   166
## Axiomatic type classes examples
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   167
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   168
AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   169
	GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   170
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   171
AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   172
	LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   173
	Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   174
	Order.ML Order.thy ROOT.ML tools.ML
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   175
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   176
AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   177
	MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   178
	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   179
	Xor.ML Xor.thy
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   180
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   181
AXCLASSES_FILES = AxClasses/ROOT.ML \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   182
	$(AXC_GROUP_FILES:%=AxClasses/Group/%) \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   183
	$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   184
	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   185
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   186
AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   187
	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
2827
cce436a62740 improved session names;
wenzelm
parents: 2826
diff changeset
   188
	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
cce436a62740 improved session names;
wenzelm
parents: 2826
diff changeset
   189
	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
cce436a62740 improved session names;
wenzelm
parents: 2826
diff changeset
   190
	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
2545
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   191
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   192
2909
22a8a97b66be Added Example Quot
slotosch
parents: 2900
diff changeset
   193
## Higher-order quotients and example fractionals
2900
d5e1a2b869a2 added Quot examples;
wenzelm
parents: 2889
diff changeset
   194
2909
22a8a97b66be Added Example Quot
slotosch
parents: 2900
diff changeset
   195
QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
22a8a97b66be Added Example Quot
slotosch
parents: 2900
diff changeset
   196
	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
22a8a97b66be Added Example Quot
slotosch
parents: 2900
diff changeset
   197
	Quot/FRACT.thy Quot/FRACT.ML
2900
d5e1a2b869a2 added Quot examples;
wenzelm
parents: 2889
diff changeset
   198
Quot:	$(OUT)/HOL $(QUOT_FILES)
d5e1a2b869a2 added Quot examples;
wenzelm
parents: 2889
diff changeset
   199
	@$(ISATOOL) usedir $(OUT)/HOL Quot
d5e1a2b869a2 added Quot examples;
wenzelm
parents: 2889
diff changeset
   200
d5e1a2b869a2 added Quot examples;
wenzelm
parents: 2889
diff changeset
   201
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   202
## Miscellaneous examples
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   203
3417
58ccb80eb50a New example theory: Recdef
paulson
parents: 3390
diff changeset
   204
EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   205
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   206
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   207
	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   208
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   209
ex:	$(OUT)/HOL $(EX_FILES)
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   210
	@$(ISATOOL) usedir $(OUT)/HOL ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   211
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   212
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   213
## Full test
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   214
2635
835820c1591d cosmetic
oheimb
parents: 2607
diff changeset
   215
test:	$(OUT)/HOL \
3218
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   216
		Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   217
		W0 MiniML IOA AxClasses Quot ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   218
	echo 'Test examples ran successfully' > test
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   219
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   220
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   221
.PRECIOUS: $(OUT)/Pure $(OUT)/HOL