# HG changeset patch
# User mueller
# Date 863791718 -7200
# Node ID 44f01b718eab2281e2d2b8e52f45c20d2f76a0e9
# Parent  d30d62128fe536a16350e2a2c14bd823081aa59b
added Modelcheck example;

diff -r d30d62128fe5 -r 44f01b718eab src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 16 15:57:11 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri May 16 16:08:38 1997 +0200
@@ -92,6 +92,16 @@
 	@$(ISATOOL) usedir $(OUT)/HOL Auth
 
 
+## Modelchecker invocation
+
+MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \
+  Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
+  Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
+
+Modelcheck: $(OUT)/HOL $(MC_FILES)
+	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
+
+
 ## Properties of substitutions
 
 SUBST_NAMES = AList Subst Unifier UTerm Unify
@@ -197,7 +207,7 @@
 ## Full test
 
 test:	$(OUT)/HOL \
-		Subst Induct IMP Hoare Lex Integ Auth Lambda  \
+		Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
 		W0 MiniML IOA AxClasses Quot ex
 	echo 'Test examples ran successfully' > test