added Modelcheck example;
authormueller
Fri May 16 16:08:38 1997 +0200 (1997-05-16)
changeset 321844f01b718eab
parent 3217 d30d62128fe5
child 3219 9854e3ea09e7
added Modelcheck example;
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Fri May 16 15:57:11 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri May 16 16:08:38 1997 +0200
     1.3 @@ -92,6 +92,16 @@
     1.4  	@$(ISATOOL) usedir $(OUT)/HOL Auth
     1.5  
     1.6  
     1.7 +## Modelchecker invocation
     1.8 +
     1.9 +MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \
    1.10 +  Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
    1.11 +  Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
    1.12 +
    1.13 +Modelcheck: $(OUT)/HOL $(MC_FILES)
    1.14 +	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
    1.15 +
    1.16 +
    1.17  ## Properties of substitutions
    1.18  
    1.19  SUBST_NAMES = AList Subst Unifier UTerm Unify
    1.20 @@ -197,7 +207,7 @@
    1.21  ## Full test
    1.22  
    1.23  test:	$(OUT)/HOL \
    1.24 -		Subst Induct IMP Hoare Lex Integ Auth Lambda  \
    1.25 +		Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
    1.26  		W0 MiniML IOA AxClasses Quot ex
    1.27  	echo 'Test examples ran successfully' > test
    1.28