# HG changeset patch
# User wenzelm
# Date 991335229 -7200
# Node ID 8fbb19b84f9474508f32002a4b0b3eca85c6cf07
# Parent  778c369559d90517f6b4bf7e19dcd45f2a2ccf5e
added HOL-CTL;

diff -r 778c369559d9 -r 8fbb19b84f94 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 31 20:52:51 2001 +0200
+++ b/src/HOL/IsaMakefile	Thu May 31 20:53:49 2001 +0200
@@ -16,6 +16,7 @@
   HOL-Auth \
   HOL-AxClasses \
   HOL-BCV \
+  HOL-CTL \
       HOL-Real-HahnBanach \
       HOL-Real-ex \
   HOL-Hoare \
@@ -459,6 +460,16 @@
   BCV/Product.ML BCV/Product.thy
 	@$(ISATOOL) usedir $(OUT)/HOL BCV
 
+
+## HOL-CTL
+
+HOL-CTL: HOL $(LOG)/HOL-CTL.gz
+
+$(LOG)/HOL-CTL.gz: $(OUT)/HOL \
+  CTL/CTL.thy CTL/ROOT.ML CTL/document/root.tex CTL/document/root.bib
+	@$(ISATOOL) usedir $(OUT)/HOL CTL
+
+
 ## HOL-IOA
 
 HOL-IOA: HOL $(LOG)/HOL-IOA.gz
@@ -579,7 +590,7 @@
 		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
 		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
 		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
-		$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
+		$(LOG)/HOL-BCV.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \