src/HOL/IsaMakefile
changeset 3819 5a6a6f18b109
parent 3616 fcd7e70258f7
child 3981 b4f93a8da835
     1.1 --- a/src/HOL/IsaMakefile	Thu Oct 09 15:00:41 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Oct 09 15:01:11 1997 +0200
     1.3 @@ -75,9 +75,43 @@
     1.4  	@$(ISATOOL) usedir $(OUT)/HOL Integ
     1.5  
     1.6  
     1.7 +## TLA -- Temporal Logic of Actions
     1.8 +
     1.9 +TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \
    1.10 +	TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \
    1.11 +	TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML
    1.12 +
    1.13 +TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy
    1.14 +
    1.15 +TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \
    1.16 +	TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML
    1.17 +
    1.18 +TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \
    1.19 +	TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \
    1.20 +	TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \
    1.21 +	TLA/Memory/Memory.ML TLA/Memory/Memory.thy \
    1.22 +	TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \
    1.23 +	TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \
    1.24 +	TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \
    1.25 +	TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \
    1.26 +	TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy
    1.27 +
    1.28 +
    1.29 +TLA: $(OUT)/HOL $(TLA_FILES)
    1.30 +	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
    1.31 +
    1.32 +TLA_Inc: $(OUT)/TLA $(TLA_INC_FILES)
    1.33 +	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
    1.34 +
    1.35 +TLA_Buffer: $(OUT)/TLA $(TLA_BUFFER_FILES)
    1.36 +	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
    1.37 +
    1.38 +TLA_Memory: $(OUT)/TLA $(TLA_MEMORY_FILES)
    1.39 +	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
    1.40 +
    1.41 +
    1.42  ## I/O Automata (meta theory only)
    1.43  
    1.44 -
    1.45  IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
    1.46    IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
    1.47  
    1.48 @@ -213,8 +247,8 @@
    1.49  ## Full test
    1.50  
    1.51  test:	$(OUT)/HOL \
    1.52 -		Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
    1.53 -		W0 MiniML IOA AxClasses Quot ex
    1.54 +	  Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
    1.55 +	  W0 MiniML TLA TLA_Inc TLA_Buffer TLA_Memory IOA AxClasses Quot ex
    1.56  	echo 'Test examples ran successfully' > test
    1.57  
    1.58