src/HOL/IsaMakefile
changeset 34996 51c93ab92c3e
parent 34974 18b41bba42b5
child 35029 22aab1c5e5a8
child 35032 7efe662e41b4
child 35070 96136eb6218f
     1.1 --- a/src/HOL/IsaMakefile	Tue Feb 02 19:26:34 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Feb 02 19:30:08 2010 +0100
     1.3 @@ -1229,167 +1229,7 @@
     1.4  HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
     1.5  
     1.6  $(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML		\
     1.7 -  SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01	\
     1.8 -  SMT/Examples/cert/z3_arith_quant_01.proof				\
     1.9 -  SMT/Examples/cert/z3_arith_quant_02					\
    1.10 -  SMT/Examples/cert/z3_arith_quant_02.proof				\
    1.11 -  SMT/Examples/cert/z3_arith_quant_03					\
    1.12 -  SMT/Examples/cert/z3_arith_quant_03.proof				\
    1.13 -  SMT/Examples/cert/z3_arith_quant_04					\
    1.14 -  SMT/Examples/cert/z3_arith_quant_04.proof				\
    1.15 -  SMT/Examples/cert/z3_arith_quant_05					\
    1.16 -  SMT/Examples/cert/z3_arith_quant_05.proof				\
    1.17 -  SMT/Examples/cert/z3_arith_quant_06					\
    1.18 -  SMT/Examples/cert/z3_arith_quant_06.proof				\
    1.19 -  SMT/Examples/cert/z3_arith_quant_07					\
    1.20 -  SMT/Examples/cert/z3_arith_quant_07.proof				\
    1.21 -  SMT/Examples/cert/z3_arith_quant_08					\
    1.22 -  SMT/Examples/cert/z3_arith_quant_08.proof				\
    1.23 -  SMT/Examples/cert/z3_arith_quant_09					\
    1.24 -  SMT/Examples/cert/z3_arith_quant_09.proof				\
    1.25 -  SMT/Examples/cert/z3_arith_quant_10					\
    1.26 -  SMT/Examples/cert/z3_arith_quant_10.proof				\
    1.27 -  SMT/Examples/cert/z3_arith_quant_11					\
    1.28 -  SMT/Examples/cert/z3_arith_quant_11.proof				\
    1.29 -  SMT/Examples/cert/z3_arith_quant_12					\
    1.30 -  SMT/Examples/cert/z3_arith_quant_12.proof				\
    1.31 -  SMT/Examples/cert/z3_arith_quant_13					\
    1.32 -  SMT/Examples/cert/z3_arith_quant_13.proof				\
    1.33 -  SMT/Examples/cert/z3_arith_quant_14					\
    1.34 -  SMT/Examples/cert/z3_arith_quant_14.proof				\
    1.35 -  SMT/Examples/cert/z3_arith_quant_15					\
    1.36 -  SMT/Examples/cert/z3_arith_quant_15.proof				\
    1.37 -  SMT/Examples/cert/z3_arith_quant_16					\
    1.38 -  SMT/Examples/cert/z3_arith_quant_16.proof				\
    1.39 -  SMT/Examples/cert/z3_arith_quant_17					\
    1.40 -  SMT/Examples/cert/z3_arith_quant_17.proof				\
    1.41 -  SMT/Examples/cert/z3_arith_quant_18					\
    1.42 -  SMT/Examples/cert/z3_arith_quant_18.proof SMT/Examples/cert/z3_bv_01	\
    1.43 -  SMT/Examples/cert/z3_bv_01.proof SMT/Examples/cert/z3_bv_02		\
    1.44 -  SMT/Examples/cert/z3_bv_02.proof SMT/Examples/cert/z3_bv_arith_01	\
    1.45 -  SMT/Examples/cert/z3_bv_arith_01.proof				\
    1.46 -  SMT/Examples/cert/z3_bv_arith_02					\
    1.47 -  SMT/Examples/cert/z3_bv_arith_02.proof				\
    1.48 -  SMT/Examples/cert/z3_bv_arith_03					\
    1.49 -  SMT/Examples/cert/z3_bv_arith_03.proof				\
    1.50 -  SMT/Examples/cert/z3_bv_arith_04					\
    1.51 -  SMT/Examples/cert/z3_bv_arith_04.proof				\
    1.52 -  SMT/Examples/cert/z3_bv_arith_05					\
    1.53 -  SMT/Examples/cert/z3_bv_arith_05.proof				\
    1.54 -  SMT/Examples/cert/z3_bv_arith_06					\
    1.55 -  SMT/Examples/cert/z3_bv_arith_06.proof				\
    1.56 -  SMT/Examples/cert/z3_bv_arith_07					\
    1.57 -  SMT/Examples/cert/z3_bv_arith_07.proof				\
    1.58 -  SMT/Examples/cert/z3_bv_arith_08					\
    1.59 -  SMT/Examples/cert/z3_bv_arith_08.proof				\
    1.60 -  SMT/Examples/cert/z3_bv_arith_09					\
    1.61 -  SMT/Examples/cert/z3_bv_arith_09.proof				\
    1.62 -  SMT/Examples/cert/z3_bv_arith_10					\
    1.63 -  SMT/Examples/cert/z3_bv_arith_10.proof				\
    1.64 -  SMT/Examples/cert/z3_bv_bit_01 SMT/Examples/cert/z3_bv_bit_01.proof	\
    1.65 -  SMT/Examples/cert/z3_bv_bit_02 SMT/Examples/cert/z3_bv_bit_02.proof	\
    1.66 -  SMT/Examples/cert/z3_bv_bit_03 SMT/Examples/cert/z3_bv_bit_03.proof	\
    1.67 -  SMT/Examples/cert/z3_bv_bit_04 SMT/Examples/cert/z3_bv_bit_04.proof	\
    1.68 -  SMT/Examples/cert/z3_bv_bit_05 SMT/Examples/cert/z3_bv_bit_05.proof	\
    1.69 -  SMT/Examples/cert/z3_bv_bit_06 SMT/Examples/cert/z3_bv_bit_06.proof	\
    1.70 -  SMT/Examples/cert/z3_bv_bit_07 SMT/Examples/cert/z3_bv_bit_07.proof	\
    1.71 -  SMT/Examples/cert/z3_bv_bit_08 SMT/Examples/cert/z3_bv_bit_08.proof	\
    1.72 -  SMT/Examples/cert/z3_bv_bit_09 SMT/Examples/cert/z3_bv_bit_09.proof	\
    1.73 -  SMT/Examples/cert/z3_bv_bit_10 SMT/Examples/cert/z3_bv_bit_10.proof	\
    1.74 -  SMT/Examples/cert/z3_bv_bit_11 SMT/Examples/cert/z3_bv_bit_11.proof	\
    1.75 -  SMT/Examples/cert/z3_bv_bit_12 SMT/Examples/cert/z3_bv_bit_12.proof	\
    1.76 -  SMT/Examples/cert/z3_bv_bit_13 SMT/Examples/cert/z3_bv_bit_13.proof	\
    1.77 -  SMT/Examples/cert/z3_bv_bit_14 SMT/Examples/cert/z3_bv_bit_14.proof	\
    1.78 -  SMT/Examples/cert/z3_bv_bit_15 SMT/Examples/cert/z3_bv_bit_15.proof	\
    1.79 -  SMT/Examples/cert/z3_fol_01 SMT/Examples/cert/z3_fol_01.proof		\
    1.80 -  SMT/Examples/cert/z3_fol_02 SMT/Examples/cert/z3_fol_02.proof		\
    1.81 -  SMT/Examples/cert/z3_fol_03 SMT/Examples/cert/z3_fol_03.proof		\
    1.82 -  SMT/Examples/cert/z3_fol_04 SMT/Examples/cert/z3_fol_04.proof		\
    1.83 -  SMT/Examples/cert/z3_hol_01 SMT/Examples/cert/z3_hol_01.proof		\
    1.84 -  SMT/Examples/cert/z3_hol_02 SMT/Examples/cert/z3_hol_02.proof		\
    1.85 -  SMT/Examples/cert/z3_hol_03 SMT/Examples/cert/z3_hol_03.proof		\
    1.86 -  SMT/Examples/cert/z3_hol_04 SMT/Examples/cert/z3_hol_04.proof		\
    1.87 -  SMT/Examples/cert/z3_hol_05 SMT/Examples/cert/z3_hol_05.proof		\
    1.88 -  SMT/Examples/cert/z3_hol_06 SMT/Examples/cert/z3_hol_06.proof		\
    1.89 -  SMT/Examples/cert/z3_hol_07 SMT/Examples/cert/z3_hol_07.proof		\
    1.90 -  SMT/Examples/cert/z3_hol_08 SMT/Examples/cert/z3_hol_08.proof		\
    1.91 -  SMT/Examples/cert/z3_linarith_01					\
    1.92 -  SMT/Examples/cert/z3_linarith_01.proof				\
    1.93 -  SMT/Examples/cert/z3_linarith_02					\
    1.94 -  SMT/Examples/cert/z3_linarith_02.proof				\
    1.95 -  SMT/Examples/cert/z3_linarith_03					\
    1.96 -  SMT/Examples/cert/z3_linarith_03.proof				\
    1.97 -  SMT/Examples/cert/z3_linarith_04					\
    1.98 -  SMT/Examples/cert/z3_linarith_04.proof				\
    1.99 -  SMT/Examples/cert/z3_linarith_05					\
   1.100 -  SMT/Examples/cert/z3_linarith_05.proof				\
   1.101 -  SMT/Examples/cert/z3_linarith_06					\
   1.102 -  SMT/Examples/cert/z3_linarith_06.proof				\
   1.103 -  SMT/Examples/cert/z3_linarith_07					\
   1.104 -  SMT/Examples/cert/z3_linarith_07.proof				\
   1.105 -  SMT/Examples/cert/z3_linarith_08					\
   1.106 -  SMT/Examples/cert/z3_linarith_08.proof				\
   1.107 -  SMT/Examples/cert/z3_linarith_09					\
   1.108 -  SMT/Examples/cert/z3_linarith_09.proof				\
   1.109 -  SMT/Examples/cert/z3_linarith_10					\
   1.110 -  SMT/Examples/cert/z3_linarith_10.proof				\
   1.111 -  SMT/Examples/cert/z3_linarith_11					\
   1.112 -  SMT/Examples/cert/z3_linarith_11.proof				\
   1.113 -  SMT/Examples/cert/z3_linarith_12					\
   1.114 -  SMT/Examples/cert/z3_linarith_12.proof				\
   1.115 -  SMT/Examples/cert/z3_linarith_13					\
   1.116 -  SMT/Examples/cert/z3_linarith_13.proof				\
   1.117 -  SMT/Examples/cert/z3_linarith_14					\
   1.118 -  SMT/Examples/cert/z3_linarith_14.proof				\
   1.119 -  SMT/Examples/cert/z3_linarith_15					\
   1.120 -  SMT/Examples/cert/z3_linarith_15.proof				\
   1.121 -  SMT/Examples/cert/z3_linarith_16					\
   1.122 -  SMT/Examples/cert/z3_linarith_16.proof				\
   1.123 -  SMT/Examples/cert/z3_linarith_17					\
   1.124 -  SMT/Examples/cert/z3_linarith_17.proof				\
   1.125 -  SMT/Examples/cert/z3_linarith_18					\
   1.126 -  SMT/Examples/cert/z3_linarith_18.proof				\
   1.127 -  SMT/Examples/cert/z3_linarith_19					\
   1.128 -  SMT/Examples/cert/z3_linarith_19.proof				\
   1.129 -  SMT/Examples/cert/z3_linarith_20					\
   1.130 -  SMT/Examples/cert/z3_linarith_20.proof 				\
   1.131 -  SMT/Examples/cert/z3_linarith_21					\
   1.132 -  SMT/Examples/cert/z3_linarith_21.proof SMT/Examples/cert/z3_mono_01	\
   1.133 -  SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02	\
   1.134 -  SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01	\
   1.135 -  SMT/Examples/cert/z3_nat_arith_01.proof				\
   1.136 -  SMT/Examples/cert/z3_nat_arith_02					\
   1.137 -  SMT/Examples/cert/z3_nat_arith_02.proof				\
   1.138 -  SMT/Examples/cert/z3_nat_arith_03					\
   1.139 -  SMT/Examples/cert/z3_nat_arith_03.proof				\
   1.140 -  SMT/Examples/cert/z3_nat_arith_04					\
   1.141 -  SMT/Examples/cert/z3_nat_arith_04.proof				\
   1.142 -  SMT/Examples/cert/z3_nat_arith_05					\
   1.143 -  SMT/Examples/cert/z3_nat_arith_05.proof				\
   1.144 -  SMT/Examples/cert/z3_nat_arith_06					\
   1.145 -  SMT/Examples/cert/z3_nat_arith_06.proof				\
   1.146 -  SMT/Examples/cert/z3_nat_arith_07					\
   1.147 -  SMT/Examples/cert/z3_nat_arith_07.proof				\
   1.148 -  SMT/Examples/cert/z3_nlarith_01					\
   1.149 -  SMT/Examples/cert/z3_nlarith_01.proof					\
   1.150 -  SMT/Examples/cert/z3_nlarith_02					\
   1.151 -  SMT/Examples/cert/z3_nlarith_02.proof					\
   1.152 -  SMT/Examples/cert/z3_nlarith_03					\
   1.153 -  SMT/Examples/cert/z3_nlarith_03.proof					\
   1.154 -  SMT/Examples/cert/z3_nlarith_04					\
   1.155 -  SMT/Examples/cert/z3_nlarith_04.proof SMT/Examples/cert/z3_pair_01	\
   1.156 -  SMT/Examples/cert/z3_pair_01.proof SMT/Examples/cert/z3_pair_02	\
   1.157 -  SMT/Examples/cert/z3_pair_02.proof SMT/Examples/cert/z3_prop_01	\
   1.158 -  SMT/Examples/cert/z3_prop_01.proof SMT/Examples/cert/z3_prop_02	\
   1.159 -  SMT/Examples/cert/z3_prop_02.proof SMT/Examples/cert/z3_prop_03	\
   1.160 -  SMT/Examples/cert/z3_prop_03.proof SMT/Examples/cert/z3_prop_04	\
   1.161 -  SMT/Examples/cert/z3_prop_04.proof SMT/Examples/cert/z3_prop_05	\
   1.162 -  SMT/Examples/cert/z3_prop_05.proof SMT/Examples/cert/z3_prop_06	\
   1.163 -  SMT/Examples/cert/z3_prop_06.proof SMT/Examples/cert/z3_prop_07	\
   1.164 -  SMT/Examples/cert/z3_prop_07.proof SMT/Examples/cert/z3_prop_08	\
   1.165 -  SMT/Examples/cert/z3_prop_08.proof SMT/Examples/cert/z3_prop_09	\
   1.166 -  SMT/Examples/cert/z3_prop_09.proof SMT/Examples/cert/z3_prop_10	\
   1.167 -  SMT/Examples/cert/z3_prop_10.proof
   1.168 +  SMT/Examples/SMT_Examples.thy SMT/Examples/SMT_Examples.certs
   1.169  	@cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples
   1.170  
   1.171  
   1.172 @@ -1411,13 +1251,8 @@
   1.173    Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy		\
   1.174    Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy	\
   1.175    Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i	\
   1.176 -  Boogie/Examples/VCC_Max.b2i Boogie/Examples/cert/Boogie_max		\
   1.177 -  Boogie/Examples/cert/Boogie_max.proof					\
   1.178 -  Boogie/Examples/cert/Boogie_Dijkstra					\
   1.179 -  Boogie/Examples/cert/Boogie_Dijkstra.proof				\
   1.180 -  Boogie/Examples/cert/VCC_maximum					\
   1.181 -  Boogie/Examples/cert/VCC_maximum.proof				\
   1.182 -  Boogie/Examples/Boogie_Max_Stepwise.thy
   1.183 +  Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs		\
   1.184 +  Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs
   1.185  	@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
   1.186  
   1.187