/src/HOL/SMT/Examples/cert/
drwxr-xr-x [up]
-rw-r--r-- 2009-10-24 19:22 +0200 85 z3_arith_quant_01
-rw-r--r-- 2009-10-24 19:22 +0200 514 z3_arith_quant_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 86 z3_arith_quant_02
-rw-r--r-- 2009-10-24 19:22 +0200 515 z3_arith_quant_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 83 z3_arith_quant_03
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_arith_quant_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 86 z3_arith_quant_04
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_arith_quant_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 104 z3_arith_quant_05
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_arith_quant_05.proof
-rw-r--r-- 2009-10-24 19:22 +0200 137 z3_arith_quant_06
-rw-r--r-- 2009-10-24 19:22 +0200 1632 z3_arith_quant_06.proof
-rw-r--r-- 2009-10-24 19:22 +0200 140 z3_arith_quant_07
-rw-r--r-- 2009-10-24 19:22 +0200 1895 z3_arith_quant_07.proof
-rw-r--r-- 2009-10-24 19:22 +0200 135 z3_arith_quant_08
-rw-r--r-- 2009-10-24 19:22 +0200 2967 z3_arith_quant_08.proof
-rw-r--r-- 2009-10-24 19:22 +0200 119 z3_arith_quant_09
-rw-r--r-- 2009-10-24 19:22 +0200 2291 z3_arith_quant_09.proof
-rw-r--r-- 2009-10-24 19:22 +0200 147 z3_arith_quant_10
-rw-r--r-- 2009-10-24 19:22 +0200 2635 z3_arith_quant_10.proof
-rw-r--r-- 2009-10-24 19:22 +0200 124 z3_arith_quant_11
-rw-r--r-- 2009-10-24 19:22 +0200 2112 z3_arith_quant_11.proof
-rw-r--r-- 2009-10-24 19:22 +0200 124 z3_arith_quant_12
-rw-r--r-- 2009-10-24 19:22 +0200 1965 z3_arith_quant_12.proof
-rw-r--r-- 2009-10-24 19:22 +0200 118 z3_arith_quant_13
-rw-r--r-- 2009-10-24 19:22 +0200 4393 z3_arith_quant_13.proof
-rw-r--r-- 2009-10-24 19:22 +0200 133 z3_arith_quant_14
-rw-r--r-- 2009-10-24 19:22 +0200 2406 z3_arith_quant_14.proof
-rw-r--r-- 2009-10-24 19:22 +0200 156 z3_arith_quant_15
-rw-r--r-- 2009-10-24 19:22 +0200 2515 z3_arith_quant_15.proof
-rw-r--r-- 2009-10-24 19:22 +0200 155 z3_arith_quant_16
-rw-r--r-- 2009-10-24 19:22 +0200 2763 z3_arith_quant_16.proof
-rw-r--r-- 2009-10-24 19:22 +0200 145 z3_arith_quant_17
-rw-r--r-- 2009-10-24 19:22 +0200 3630 z3_arith_quant_17.proof
-rw-r--r-- 2009-10-24 19:22 +0200 162 z3_arith_quant_18
-rw-r--r-- 2009-10-24 19:22 +0200 2567 z3_arith_quant_18.proof
-rw-r--r-- 2009-10-24 19:22 +0200 358 z3_bv_01
-rw-r--r-- 2009-10-24 19:22 +0200 1035 z3_bv_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 310 z3_bv_02
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 81 z3_bv_arith_01
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 74 z3_bv_arith_02
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 78 z3_bv_arith_03
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 89 z3_bv_arith_04
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 88 z3_bv_arith_05
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_05.proof
-rw-r--r-- 2009-10-24 19:22 +0200 98 z3_bv_arith_06
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_06.proof
-rw-r--r-- 2009-10-24 19:22 +0200 90 z3_bv_arith_07
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_07.proof
-rw-r--r-- 2009-10-24 19:22 +0200 105 z3_bv_arith_08
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_08.proof
-rw-r--r-- 2009-10-24 19:22 +0200 225 z3_bv_arith_09
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_09.proof
-rw-r--r-- 2009-10-24 19:22 +0200 148 z3_bv_arith_10
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_arith_10.proof
-rw-r--r-- 2009-10-24 19:22 +0200 90 z3_bv_bit_01
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 86 z3_bv_bit_02
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 92 z3_bv_bit_03
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 88 z3_bv_bit_04
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 94 z3_bv_bit_05
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_05.proof
-rw-r--r-- 2009-10-24 19:22 +0200 92 z3_bv_bit_06
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_06.proof
-rw-r--r-- 2009-10-24 19:22 +0200 363 z3_bv_bit_07
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_07.proof
-rw-r--r-- 2009-10-24 19:22 +0200 92 z3_bv_bit_08
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_08.proof
-rw-r--r-- 2009-10-24 19:22 +0200 91 z3_bv_bit_09
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_09.proof
-rw-r--r-- 2009-10-24 19:22 +0200 89 z3_bv_bit_10
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_10.proof
-rw-r--r-- 2009-10-24 19:22 +0200 89 z3_bv_bit_11
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_11.proof
-rw-r--r-- 2009-10-24 19:22 +0200 365 z3_bv_bit_12
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_12.proof
-rw-r--r-- 2009-10-24 19:22 +0200 366 z3_bv_bit_13
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_13.proof
-rw-r--r-- 2009-10-24 19:22 +0200 154 z3_bv_bit_14
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_14.proof
-rw-r--r-- 2009-10-24 19:22 +0200 157 z3_bv_bit_15
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_bv_bit_15.proof
-rw-r--r-- 2009-10-24 19:22 +0200 188 z3_fol_01
-rw-r--r-- 2009-10-24 19:22 +0200 1730 z3_fol_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 289 z3_fol_02
-rw-r--r-- 2009-10-24 19:22 +0200 3320 z3_fol_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 392 z3_fol_03
-rw-r--r-- 2009-10-24 19:22 +0200 3393 z3_fol_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 287 z3_fol_04
-rw-r--r-- 2009-10-24 19:22 +0200 1245 z3_fol_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 549 z3_hol_01
-rw-r--r-- 2009-10-24 19:22 +0200 4577 z3_hol_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 282 z3_hol_02
-rw-r--r-- 2009-10-24 19:22 +0200 1351 z3_hol_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 322 z3_hol_03
-rw-r--r-- 2009-10-24 19:22 +0200 2811 z3_hol_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 549 z3_hol_04
-rw-r--r-- 2009-10-24 19:22 +0200 4577 z3_hol_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 747 z3_hol_05
-rw-r--r-- 2009-10-24 19:22 +0200 11935 z3_hol_05.proof
-rw-r--r-- 2009-10-24 19:22 +0200 173 z3_hol_06
-rw-r--r-- 2009-10-24 19:22 +0200 419 z3_hol_06.proof
-rw-r--r-- 2009-10-24 19:22 +0200 505 z3_hol_07
-rw-r--r-- 2009-10-24 19:22 +0200 9554 z3_hol_07.proof
-rw-r--r-- 2009-10-24 19:22 +0200 1008 z3_hol_08
-rw-r--r-- 2009-10-24 19:22 +0200 10916 z3_hol_08.proof
-rw-r--r-- 2009-10-24 19:22 +0200 62 z3_linarith_01
-rw-r--r-- 2009-10-24 19:22 +0200 330 z3_linarith_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 66 z3_linarith_02
-rw-r--r-- 2009-10-24 19:22 +0200 333 z3_linarith_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 68 z3_linarith_03
-rw-r--r-- 2009-10-24 19:22 +0200 523 z3_linarith_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 159 z3_linarith_04
-rw-r--r-- 2009-10-24 19:22 +0200 814 z3_linarith_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 79 z3_linarith_05
-rw-r--r-- 2009-10-24 19:22 +0200 753 z3_linarith_05.proof
-rw-r--r-- 2009-10-24 19:22 +0200 233 z3_linarith_06
-rw-r--r-- 2009-10-24 19:22 +0200 6495 z3_linarith_06.proof
-rw-r--r-- 2009-10-24 19:22 +0200 255 z3_linarith_07
-rw-r--r-- 2009-10-24 19:22 +0200 2546 z3_linarith_07.proof
-rw-r--r-- 2009-10-24 19:22 +0200 117 z3_linarith_08
-rw-r--r-- 2009-10-24 19:22 +0200 1145 z3_linarith_08.proof
-rw-r--r-- 2009-10-24 19:22 +0200 172 z3_linarith_09
-rw-r--r-- 2009-10-24 19:22 +0200 1338 z3_linarith_09.proof
-rw-r--r-- 2009-10-24 19:22 +0200 92 z3_linarith_10
-rw-r--r-- 2009-10-24 19:22 +0200 726 z3_linarith_10.proof
-rw-r--r-- 2009-10-24 19:22 +0200 194 z3_linarith_11
-rw-r--r-- 2009-10-24 19:22 +0200 911 z3_linarith_11.proof
-rw-r--r-- 2009-10-24 19:22 +0200 185 z3_linarith_12
-rw-r--r-- 2009-10-24 19:22 +0200 1244 z3_linarith_12.proof
-rw-r--r-- 2009-10-24 19:22 +0200 359 z3_linarith_13
-rw-r--r-- 2009-10-24 19:22 +0200 5410 z3_linarith_13.proof
-rw-r--r-- 2009-10-24 19:22 +0200 147 z3_linarith_14
-rw-r--r-- 2009-10-24 19:22 +0200 2025 z3_linarith_14.proof
-rw-r--r-- 2009-10-24 19:22 +0200 728 z3_linarith_15
-rw-r--r-- 2009-10-24 19:22 +0200 17376 z3_linarith_15.proof
-rw-r--r-- 2009-10-24 19:22 +0200 805 z3_linarith_16
-rw-r--r-- 2009-10-24 19:22 +0200 82869 z3_linarith_16.proof
-rw-r--r-- 2009-10-24 19:22 +0200 2049 z3_mono_01
-rw-r--r-- 2009-10-24 19:22 +0200 1250 z3_mono_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 1720 z3_mono_02
-rw-r--r-- 2009-10-24 19:22 +0200 12620 z3_mono_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 373 z3_nat_arith_01
-rw-r--r-- 2009-10-24 19:22 +0200 6218 z3_nat_arith_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 409 z3_nat_arith_02
-rw-r--r-- 2009-10-24 19:22 +0200 4924 z3_nat_arith_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 454 z3_nat_arith_03
-rw-r--r-- 2009-10-24 19:22 +0200 9283 z3_nat_arith_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 489 z3_nat_arith_04
-rw-r--r-- 2009-10-24 19:22 +0200 7633 z3_nat_arith_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 457 z3_nat_arith_05
-rw-r--r-- 2009-10-24 19:22 +0200 13940 z3_nat_arith_05.proof
-rw-r--r-- 2009-10-24 19:22 +0200 422 z3_nat_arith_06
-rw-r--r-- 2009-10-24 19:22 +0200 4010 z3_nat_arith_06.proof
-rw-r--r-- 2009-10-24 19:22 +0200 618 z3_nat_arith_07
-rw-r--r-- 2009-10-24 19:22 +0200 14252 z3_nat_arith_07.proof
-rw-r--r-- 2009-10-24 19:22 +0200 162 z3_nlarith_01
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_nlarith_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 180 z3_nlarith_02
-rw-r--r-- 2009-10-24 19:22 +0200 1561 z3_nlarith_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 172 z3_nlarith_03
-rw-r--r-- 2009-10-24 19:22 +0200 1287 z3_nlarith_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 323 z3_nlarith_04
-rw-r--r-- 2009-10-24 19:22 +0200 3028 z3_nlarith_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 442 z3_pair_01
-rw-r--r-- 2009-10-24 19:22 +0200 1159 z3_pair_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 754 z3_pair_02
-rw-r--r-- 2009-10-24 19:22 +0200 2558 z3_pair_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 59 z3_prop_01
-rw-r--r-- 2009-10-24 19:22 +0200 132 z3_prop_01.proof
-rw-r--r-- 2009-10-24 19:22 +0200 119 z3_prop_02
-rw-r--r-- 2009-10-24 19:22 +0200 358 z3_prop_02.proof
-rw-r--r-- 2009-10-24 19:22 +0200 125 z3_prop_03
-rw-r--r-- 2009-10-24 19:22 +0200 509 z3_prop_03.proof
-rw-r--r-- 2009-10-24 19:22 +0200 156 z3_prop_04
-rw-r--r-- 2009-10-24 19:22 +0200 793 z3_prop_04.proof
-rw-r--r-- 2009-10-24 19:22 +0200 211 z3_prop_05
-rw-r--r-- 2009-10-24 19:22 +0200 6 z3_prop_05.proof
-rw-r--r-- 2009-10-24 19:22 +0200 214 z3_prop_06
-rw-r--r-- 2009-10-24 19:22 +0200 1529 z3_prop_06.proof
-rw-r--r-- 2009-10-24 19:22 +0200 202 z3_prop_07
-rw-r--r-- 2009-10-24 19:22 +0200 1299 z3_prop_07.proof
-rw-r--r-- 2009-10-24 19:22 +0200 512 z3_prop_08
-rw-r--r-- 2009-10-24 19:22 +0200 4626 z3_prop_08.proof
-rw-r--r-- 2009-10-24 19:22 +0200 261 z3_prop_09
-rw-r--r-- 2009-10-24 19:22 +0200 1159 z3_prop_09.proof
-rw-r--r-- 2009-10-24 19:22 +0200 8234 z3_prop_10
-rw-r--r-- 2009-10-24 19:22 +0200 56942 z3_prop_10.proof