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