src/HOL/IsaMakefile
changeset 4777 379f32b0ae40
parent 4729 e1888c0d3b36
child 4830 bd73675adbed
equal deleted inserted replaced
4776:1f9362e769c1 4777:379f32b0ae40
     7 ## targets
     7 ## targets
     8 
     8 
     9 default: HOL
     9 default: HOL
    10 images: HOL TLA
    10 images: HOL TLA
    11 test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Integ \
    11 test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Integ \
    12   HOL-Auth HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
    12   HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \
    13   HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
    13   HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \
    14   HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory
    14   HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory
    15 all: images test
    15 all: images test
    16 
    16 
    17 
    17 
   138   Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \
   138   Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \
   139   Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy
   139   Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy
   140 	@$(ISATOOL) usedir $(OUT)/HOL Auth
   140 	@$(ISATOOL) usedir $(OUT)/HOL Auth
   141 
   141 
   142 
   142 
       
   143 ## HOL-UNITY
       
   144 
       
   145 HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
       
   146 
       
   147 $(LOG)/HOL-UNITY.gz: $(OUT)/HOL UNITY/ROOT.ML\
       
   148   UNITY/Channel.ML UNITY/Channel.thy UNITY/Common.ML UNITY/Common.thy\
       
   149   UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
       
   150   UNITY/LessThan.ML UNITY/LessThan.thy UNITY/Mutex.ML UNITY/Mutex.thy\
       
   151   UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
       
   152   UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
       
   153   UNITY/Traces.ML UNITY/Traces.thy UNITY/UNITY.ML UNITY/UNITY.thy\
       
   154   UNITY/Update.ML UNITY/Update.thy UNITY/WFair.ML UNITY/WFair.thy
       
   155 	@$(ISATOOL) usedir $(OUT)/HOL UNITY
       
   156 
       
   157 
   143 ## HOL-Modelcheck
   158 ## HOL-Modelcheck
   144 
   159 
   145 HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
   160 HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
   146 
   161 
   147 $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
   162 $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
   314 ## clean
   329 ## clean
   315 
   330 
   316 clean:
   331 clean:
   317 	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
   332 	@rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
   318 	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
   333 	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
   319 	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz \
   334 	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz \
       
   335 	  $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
   320 	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
   336 	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \
   321 	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
   337 	  $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
   322 	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
   338 	  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
   323 	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
   339 	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
   324 	  $(LOG)/HOL-ex.gz $(OUT)/TLA $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz \
   340 	  $(LOG)/HOL-ex.gz $(OUT)/TLA $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz \