# HG changeset patch
# User wenzelm
# Date 876402071 -7200
# Node ID 5a6a6f18b109ec115c64c46eb20d37bd6dfdb795
# Parent  5a1116b69196d2cfa0dbcd1110cad2934225f442
added TLA stuff;

diff -r 5a1116b69196 -r 5a6a6f18b109 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Oct 09 15:00:41 1997 +0200
+++ b/src/HOL/IsaMakefile	Thu Oct 09 15:01:11 1997 +0200
@@ -75,9 +75,43 @@
 	@$(ISATOOL) usedir $(OUT)/HOL Integ
 
 
+## TLA -- Temporal Logic of Actions
+
+TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \
+	TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \
+	TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML
+
+TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy
+
+TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \
+	TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML
+
+TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \
+	TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \
+	TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \
+	TLA/Memory/Memory.ML TLA/Memory/Memory.thy \
+	TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \
+	TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \
+	TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \
+	TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \
+	TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy
+
+
+TLA: $(OUT)/HOL $(TLA_FILES)
+	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
+
+TLA_Inc: $(OUT)/TLA $(TLA_INC_FILES)
+	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
+
+TLA_Buffer: $(OUT)/TLA $(TLA_BUFFER_FILES)
+	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
+
+TLA_Memory: $(OUT)/TLA $(TLA_MEMORY_FILES)
+	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
+
+
 ## I/O Automata (meta theory only)
 
-
 IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
   IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
 
@@ -213,8 +247,8 @@
 ## Full test
 
 test:	$(OUT)/HOL \
-		Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
-		W0 MiniML IOA AxClasses Quot ex
+	  Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
+	  W0 MiniML TLA TLA_Inc TLA_Buffer TLA_Memory IOA AxClasses Quot ex
 	echo 'Test examples ran successfully' > test