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