--- a/src/HOL/IsaMakefile Tue Feb 02 19:26:34 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 02 19:30:08 2010 +0100
@@ -1229,167 +1229,7 @@
HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \
- SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \
- SMT/Examples/cert/z3_arith_quant_01.proof \
- SMT/Examples/cert/z3_arith_quant_02 \
- SMT/Examples/cert/z3_arith_quant_02.proof \
- SMT/Examples/cert/z3_arith_quant_03 \
- SMT/Examples/cert/z3_arith_quant_03.proof \
- SMT/Examples/cert/z3_arith_quant_04 \
- SMT/Examples/cert/z3_arith_quant_04.proof \
- SMT/Examples/cert/z3_arith_quant_05 \
- SMT/Examples/cert/z3_arith_quant_05.proof \
- SMT/Examples/cert/z3_arith_quant_06 \
- SMT/Examples/cert/z3_arith_quant_06.proof \
- SMT/Examples/cert/z3_arith_quant_07 \
- SMT/Examples/cert/z3_arith_quant_07.proof \
- SMT/Examples/cert/z3_arith_quant_08 \
- SMT/Examples/cert/z3_arith_quant_08.proof \
- SMT/Examples/cert/z3_arith_quant_09 \
- SMT/Examples/cert/z3_arith_quant_09.proof \
- SMT/Examples/cert/z3_arith_quant_10 \
- SMT/Examples/cert/z3_arith_quant_10.proof \
- SMT/Examples/cert/z3_arith_quant_11 \
- SMT/Examples/cert/z3_arith_quant_11.proof \
- SMT/Examples/cert/z3_arith_quant_12 \
- SMT/Examples/cert/z3_arith_quant_12.proof \
- SMT/Examples/cert/z3_arith_quant_13 \
- SMT/Examples/cert/z3_arith_quant_13.proof \
- SMT/Examples/cert/z3_arith_quant_14 \
- SMT/Examples/cert/z3_arith_quant_14.proof \
- SMT/Examples/cert/z3_arith_quant_15 \
- SMT/Examples/cert/z3_arith_quant_15.proof \
- SMT/Examples/cert/z3_arith_quant_16 \
- SMT/Examples/cert/z3_arith_quant_16.proof \
- SMT/Examples/cert/z3_arith_quant_17 \
- SMT/Examples/cert/z3_arith_quant_17.proof \
- SMT/Examples/cert/z3_arith_quant_18 \
- SMT/Examples/cert/z3_arith_quant_18.proof SMT/Examples/cert/z3_bv_01 \
- SMT/Examples/cert/z3_bv_01.proof SMT/Examples/cert/z3_bv_02 \
- SMT/Examples/cert/z3_bv_02.proof SMT/Examples/cert/z3_bv_arith_01 \
- SMT/Examples/cert/z3_bv_arith_01.proof \
- SMT/Examples/cert/z3_bv_arith_02 \
- SMT/Examples/cert/z3_bv_arith_02.proof \
- SMT/Examples/cert/z3_bv_arith_03 \
- SMT/Examples/cert/z3_bv_arith_03.proof \
- SMT/Examples/cert/z3_bv_arith_04 \
- SMT/Examples/cert/z3_bv_arith_04.proof \
- SMT/Examples/cert/z3_bv_arith_05 \
- SMT/Examples/cert/z3_bv_arith_05.proof \
- SMT/Examples/cert/z3_bv_arith_06 \
- SMT/Examples/cert/z3_bv_arith_06.proof \
- SMT/Examples/cert/z3_bv_arith_07 \
- SMT/Examples/cert/z3_bv_arith_07.proof \
- SMT/Examples/cert/z3_bv_arith_08 \
- SMT/Examples/cert/z3_bv_arith_08.proof \
- SMT/Examples/cert/z3_bv_arith_09 \
- SMT/Examples/cert/z3_bv_arith_09.proof \
- SMT/Examples/cert/z3_bv_arith_10 \
- SMT/Examples/cert/z3_bv_arith_10.proof \
- SMT/Examples/cert/z3_bv_bit_01 SMT/Examples/cert/z3_bv_bit_01.proof \
- SMT/Examples/cert/z3_bv_bit_02 SMT/Examples/cert/z3_bv_bit_02.proof \
- SMT/Examples/cert/z3_bv_bit_03 SMT/Examples/cert/z3_bv_bit_03.proof \
- SMT/Examples/cert/z3_bv_bit_04 SMT/Examples/cert/z3_bv_bit_04.proof \
- SMT/Examples/cert/z3_bv_bit_05 SMT/Examples/cert/z3_bv_bit_05.proof \
- SMT/Examples/cert/z3_bv_bit_06 SMT/Examples/cert/z3_bv_bit_06.proof \
- SMT/Examples/cert/z3_bv_bit_07 SMT/Examples/cert/z3_bv_bit_07.proof \
- SMT/Examples/cert/z3_bv_bit_08 SMT/Examples/cert/z3_bv_bit_08.proof \
- SMT/Examples/cert/z3_bv_bit_09 SMT/Examples/cert/z3_bv_bit_09.proof \
- SMT/Examples/cert/z3_bv_bit_10 SMT/Examples/cert/z3_bv_bit_10.proof \
- SMT/Examples/cert/z3_bv_bit_11 SMT/Examples/cert/z3_bv_bit_11.proof \
- SMT/Examples/cert/z3_bv_bit_12 SMT/Examples/cert/z3_bv_bit_12.proof \
- SMT/Examples/cert/z3_bv_bit_13 SMT/Examples/cert/z3_bv_bit_13.proof \
- SMT/Examples/cert/z3_bv_bit_14 SMT/Examples/cert/z3_bv_bit_14.proof \
- SMT/Examples/cert/z3_bv_bit_15 SMT/Examples/cert/z3_bv_bit_15.proof \
- SMT/Examples/cert/z3_fol_01 SMT/Examples/cert/z3_fol_01.proof \
- SMT/Examples/cert/z3_fol_02 SMT/Examples/cert/z3_fol_02.proof \
- SMT/Examples/cert/z3_fol_03 SMT/Examples/cert/z3_fol_03.proof \
- SMT/Examples/cert/z3_fol_04 SMT/Examples/cert/z3_fol_04.proof \
- SMT/Examples/cert/z3_hol_01 SMT/Examples/cert/z3_hol_01.proof \
- SMT/Examples/cert/z3_hol_02 SMT/Examples/cert/z3_hol_02.proof \
- SMT/Examples/cert/z3_hol_03 SMT/Examples/cert/z3_hol_03.proof \
- SMT/Examples/cert/z3_hol_04 SMT/Examples/cert/z3_hol_04.proof \
- SMT/Examples/cert/z3_hol_05 SMT/Examples/cert/z3_hol_05.proof \
- SMT/Examples/cert/z3_hol_06 SMT/Examples/cert/z3_hol_06.proof \
- SMT/Examples/cert/z3_hol_07 SMT/Examples/cert/z3_hol_07.proof \
- SMT/Examples/cert/z3_hol_08 SMT/Examples/cert/z3_hol_08.proof \
- SMT/Examples/cert/z3_linarith_01 \
- SMT/Examples/cert/z3_linarith_01.proof \
- SMT/Examples/cert/z3_linarith_02 \
- SMT/Examples/cert/z3_linarith_02.proof \
- SMT/Examples/cert/z3_linarith_03 \
- SMT/Examples/cert/z3_linarith_03.proof \
- SMT/Examples/cert/z3_linarith_04 \
- SMT/Examples/cert/z3_linarith_04.proof \
- SMT/Examples/cert/z3_linarith_05 \
- SMT/Examples/cert/z3_linarith_05.proof \
- SMT/Examples/cert/z3_linarith_06 \
- SMT/Examples/cert/z3_linarith_06.proof \
- SMT/Examples/cert/z3_linarith_07 \
- SMT/Examples/cert/z3_linarith_07.proof \
- SMT/Examples/cert/z3_linarith_08 \
- SMT/Examples/cert/z3_linarith_08.proof \
- SMT/Examples/cert/z3_linarith_09 \
- SMT/Examples/cert/z3_linarith_09.proof \
- SMT/Examples/cert/z3_linarith_10 \
- SMT/Examples/cert/z3_linarith_10.proof \
- SMT/Examples/cert/z3_linarith_11 \
- SMT/Examples/cert/z3_linarith_11.proof \
- SMT/Examples/cert/z3_linarith_12 \
- SMT/Examples/cert/z3_linarith_12.proof \
- SMT/Examples/cert/z3_linarith_13 \
- SMT/Examples/cert/z3_linarith_13.proof \
- SMT/Examples/cert/z3_linarith_14 \
- SMT/Examples/cert/z3_linarith_14.proof \
- SMT/Examples/cert/z3_linarith_15 \
- SMT/Examples/cert/z3_linarith_15.proof \
- SMT/Examples/cert/z3_linarith_16 \
- SMT/Examples/cert/z3_linarith_16.proof \
- SMT/Examples/cert/z3_linarith_17 \
- SMT/Examples/cert/z3_linarith_17.proof \
- SMT/Examples/cert/z3_linarith_18 \
- SMT/Examples/cert/z3_linarith_18.proof \
- SMT/Examples/cert/z3_linarith_19 \
- SMT/Examples/cert/z3_linarith_19.proof \
- SMT/Examples/cert/z3_linarith_20 \
- SMT/Examples/cert/z3_linarith_20.proof \
- SMT/Examples/cert/z3_linarith_21 \
- SMT/Examples/cert/z3_linarith_21.proof SMT/Examples/cert/z3_mono_01 \
- SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02 \
- SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01 \
- SMT/Examples/cert/z3_nat_arith_01.proof \
- SMT/Examples/cert/z3_nat_arith_02 \
- SMT/Examples/cert/z3_nat_arith_02.proof \
- SMT/Examples/cert/z3_nat_arith_03 \
- SMT/Examples/cert/z3_nat_arith_03.proof \
- SMT/Examples/cert/z3_nat_arith_04 \
- SMT/Examples/cert/z3_nat_arith_04.proof \
- SMT/Examples/cert/z3_nat_arith_05 \
- SMT/Examples/cert/z3_nat_arith_05.proof \
- SMT/Examples/cert/z3_nat_arith_06 \
- SMT/Examples/cert/z3_nat_arith_06.proof \
- SMT/Examples/cert/z3_nat_arith_07 \
- SMT/Examples/cert/z3_nat_arith_07.proof \
- SMT/Examples/cert/z3_nlarith_01 \
- SMT/Examples/cert/z3_nlarith_01.proof \
- SMT/Examples/cert/z3_nlarith_02 \
- SMT/Examples/cert/z3_nlarith_02.proof \
- SMT/Examples/cert/z3_nlarith_03 \
- SMT/Examples/cert/z3_nlarith_03.proof \
- SMT/Examples/cert/z3_nlarith_04 \
- SMT/Examples/cert/z3_nlarith_04.proof SMT/Examples/cert/z3_pair_01 \
- SMT/Examples/cert/z3_pair_01.proof SMT/Examples/cert/z3_pair_02 \
- SMT/Examples/cert/z3_pair_02.proof SMT/Examples/cert/z3_prop_01 \
- SMT/Examples/cert/z3_prop_01.proof SMT/Examples/cert/z3_prop_02 \
- SMT/Examples/cert/z3_prop_02.proof SMT/Examples/cert/z3_prop_03 \
- SMT/Examples/cert/z3_prop_03.proof SMT/Examples/cert/z3_prop_04 \
- SMT/Examples/cert/z3_prop_04.proof SMT/Examples/cert/z3_prop_05 \
- SMT/Examples/cert/z3_prop_05.proof SMT/Examples/cert/z3_prop_06 \
- SMT/Examples/cert/z3_prop_06.proof SMT/Examples/cert/z3_prop_07 \
- SMT/Examples/cert/z3_prop_07.proof SMT/Examples/cert/z3_prop_08 \
- SMT/Examples/cert/z3_prop_08.proof SMT/Examples/cert/z3_prop_09 \
- SMT/Examples/cert/z3_prop_09.proof SMT/Examples/cert/z3_prop_10 \
- SMT/Examples/cert/z3_prop_10.proof
+ SMT/Examples/SMT_Examples.thy SMT/Examples/SMT_Examples.certs
@cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples
@@ -1411,13 +1251,8 @@
Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy \
Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy \
Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i \
- Boogie/Examples/VCC_Max.b2i Boogie/Examples/cert/Boogie_max \
- Boogie/Examples/cert/Boogie_max.proof \
- Boogie/Examples/cert/Boogie_Dijkstra \
- Boogie/Examples/cert/Boogie_Dijkstra.proof \
- Boogie/Examples/cert/VCC_maximum \
- Boogie/Examples/cert/VCC_maximum.proof \
- Boogie/Examples/Boogie_Max_Stepwise.thy
+ Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs \
+ Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs
@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples