src/HOL/IsaMakefile
changeset 33197 de6285ebcc05
parent 33192 08a39a957ed7
child 33201 e3d741e9d2fe
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 23 18:57:35 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 23 18:59:24 2009 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4    HOL-Mirabelle \
     1.5    HOL-Modelcheck \
     1.6    HOL-NanoJava \
     1.7 +  HOL-Nitpick_Examples \
     1.8    HOL-Nominal-Examples \
     1.9    HOL-Number_Theory \
    1.10    HOL-Old_Number_Theory \
    1.11 @@ -43,9 +44,9 @@
    1.12    HOL-SMT-Examples \
    1.13    HOL-Statespace \
    1.14    HOL-Subst \
    1.15 -      TLA-Buffer \
    1.16 -      TLA-Inc \
    1.17 -      TLA-Memory \
    1.18 +  TLA-Buffer \
    1.19 +  TLA-Inc \
    1.20 +  TLA-Memory \
    1.21    HOL-UNITY \
    1.22    HOL-Unix \
    1.23    HOL-W0 \
    1.24 @@ -584,6 +585,21 @@
    1.25  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
    1.26  
    1.27  
    1.28 +## HOL-Nitpick_Examples
    1.29 +
    1.30 +HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
    1.31 +
    1.32 +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
    1.33 +  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
    1.34 +  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \
    1.35 +  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
    1.36 +  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
    1.37 +  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
    1.38 +  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
    1.39 +  Nitpick_Examples/Typedef_Nits.thy
    1.40 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
    1.41 +
    1.42 +
    1.43  ## HOL-Algebra
    1.44  
    1.45  HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz