1227 ## HOL-SMT-Examples |
1227 ## HOL-SMT-Examples |
1228 |
1228 |
1229 HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz |
1229 HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz |
1230 |
1230 |
1231 $(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \ |
1231 $(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \ |
1232 SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \ |
1232 SMT/Examples/SMT_Examples.thy SMT/Examples/SMT_Examples.certs |
1233 SMT/Examples/cert/z3_arith_quant_01.proof \ |
|
1234 SMT/Examples/cert/z3_arith_quant_02 \ |
|
1235 SMT/Examples/cert/z3_arith_quant_02.proof \ |
|
1236 SMT/Examples/cert/z3_arith_quant_03 \ |
|
1237 SMT/Examples/cert/z3_arith_quant_03.proof \ |
|
1238 SMT/Examples/cert/z3_arith_quant_04 \ |
|
1239 SMT/Examples/cert/z3_arith_quant_04.proof \ |
|
1240 SMT/Examples/cert/z3_arith_quant_05 \ |
|
1241 SMT/Examples/cert/z3_arith_quant_05.proof \ |
|
1242 SMT/Examples/cert/z3_arith_quant_06 \ |
|
1243 SMT/Examples/cert/z3_arith_quant_06.proof \ |
|
1244 SMT/Examples/cert/z3_arith_quant_07 \ |
|
1245 SMT/Examples/cert/z3_arith_quant_07.proof \ |
|
1246 SMT/Examples/cert/z3_arith_quant_08 \ |
|
1247 SMT/Examples/cert/z3_arith_quant_08.proof \ |
|
1248 SMT/Examples/cert/z3_arith_quant_09 \ |
|
1249 SMT/Examples/cert/z3_arith_quant_09.proof \ |
|
1250 SMT/Examples/cert/z3_arith_quant_10 \ |
|
1251 SMT/Examples/cert/z3_arith_quant_10.proof \ |
|
1252 SMT/Examples/cert/z3_arith_quant_11 \ |
|
1253 SMT/Examples/cert/z3_arith_quant_11.proof \ |
|
1254 SMT/Examples/cert/z3_arith_quant_12 \ |
|
1255 SMT/Examples/cert/z3_arith_quant_12.proof \ |
|
1256 SMT/Examples/cert/z3_arith_quant_13 \ |
|
1257 SMT/Examples/cert/z3_arith_quant_13.proof \ |
|
1258 SMT/Examples/cert/z3_arith_quant_14 \ |
|
1259 SMT/Examples/cert/z3_arith_quant_14.proof \ |
|
1260 SMT/Examples/cert/z3_arith_quant_15 \ |
|
1261 SMT/Examples/cert/z3_arith_quant_15.proof \ |
|
1262 SMT/Examples/cert/z3_arith_quant_16 \ |
|
1263 SMT/Examples/cert/z3_arith_quant_16.proof \ |
|
1264 SMT/Examples/cert/z3_arith_quant_17 \ |
|
1265 SMT/Examples/cert/z3_arith_quant_17.proof \ |
|
1266 SMT/Examples/cert/z3_arith_quant_18 \ |
|
1267 SMT/Examples/cert/z3_arith_quant_18.proof SMT/Examples/cert/z3_bv_01 \ |
|
1268 SMT/Examples/cert/z3_bv_01.proof SMT/Examples/cert/z3_bv_02 \ |
|
1269 SMT/Examples/cert/z3_bv_02.proof SMT/Examples/cert/z3_bv_arith_01 \ |
|
1270 SMT/Examples/cert/z3_bv_arith_01.proof \ |
|
1271 SMT/Examples/cert/z3_bv_arith_02 \ |
|
1272 SMT/Examples/cert/z3_bv_arith_02.proof \ |
|
1273 SMT/Examples/cert/z3_bv_arith_03 \ |
|
1274 SMT/Examples/cert/z3_bv_arith_03.proof \ |
|
1275 SMT/Examples/cert/z3_bv_arith_04 \ |
|
1276 SMT/Examples/cert/z3_bv_arith_04.proof \ |
|
1277 SMT/Examples/cert/z3_bv_arith_05 \ |
|
1278 SMT/Examples/cert/z3_bv_arith_05.proof \ |
|
1279 SMT/Examples/cert/z3_bv_arith_06 \ |
|
1280 SMT/Examples/cert/z3_bv_arith_06.proof \ |
|
1281 SMT/Examples/cert/z3_bv_arith_07 \ |
|
1282 SMT/Examples/cert/z3_bv_arith_07.proof \ |
|
1283 SMT/Examples/cert/z3_bv_arith_08 \ |
|
1284 SMT/Examples/cert/z3_bv_arith_08.proof \ |
|
1285 SMT/Examples/cert/z3_bv_arith_09 \ |
|
1286 SMT/Examples/cert/z3_bv_arith_09.proof \ |
|
1287 SMT/Examples/cert/z3_bv_arith_10 \ |
|
1288 SMT/Examples/cert/z3_bv_arith_10.proof \ |
|
1289 SMT/Examples/cert/z3_bv_bit_01 SMT/Examples/cert/z3_bv_bit_01.proof \ |
|
1290 SMT/Examples/cert/z3_bv_bit_02 SMT/Examples/cert/z3_bv_bit_02.proof \ |
|
1291 SMT/Examples/cert/z3_bv_bit_03 SMT/Examples/cert/z3_bv_bit_03.proof \ |
|
1292 SMT/Examples/cert/z3_bv_bit_04 SMT/Examples/cert/z3_bv_bit_04.proof \ |
|
1293 SMT/Examples/cert/z3_bv_bit_05 SMT/Examples/cert/z3_bv_bit_05.proof \ |
|
1294 SMT/Examples/cert/z3_bv_bit_06 SMT/Examples/cert/z3_bv_bit_06.proof \ |
|
1295 SMT/Examples/cert/z3_bv_bit_07 SMT/Examples/cert/z3_bv_bit_07.proof \ |
|
1296 SMT/Examples/cert/z3_bv_bit_08 SMT/Examples/cert/z3_bv_bit_08.proof \ |
|
1297 SMT/Examples/cert/z3_bv_bit_09 SMT/Examples/cert/z3_bv_bit_09.proof \ |
|
1298 SMT/Examples/cert/z3_bv_bit_10 SMT/Examples/cert/z3_bv_bit_10.proof \ |
|
1299 SMT/Examples/cert/z3_bv_bit_11 SMT/Examples/cert/z3_bv_bit_11.proof \ |
|
1300 SMT/Examples/cert/z3_bv_bit_12 SMT/Examples/cert/z3_bv_bit_12.proof \ |
|
1301 SMT/Examples/cert/z3_bv_bit_13 SMT/Examples/cert/z3_bv_bit_13.proof \ |
|
1302 SMT/Examples/cert/z3_bv_bit_14 SMT/Examples/cert/z3_bv_bit_14.proof \ |
|
1303 SMT/Examples/cert/z3_bv_bit_15 SMT/Examples/cert/z3_bv_bit_15.proof \ |
|
1304 SMT/Examples/cert/z3_fol_01 SMT/Examples/cert/z3_fol_01.proof \ |
|
1305 SMT/Examples/cert/z3_fol_02 SMT/Examples/cert/z3_fol_02.proof \ |
|
1306 SMT/Examples/cert/z3_fol_03 SMT/Examples/cert/z3_fol_03.proof \ |
|
1307 SMT/Examples/cert/z3_fol_04 SMT/Examples/cert/z3_fol_04.proof \ |
|
1308 SMT/Examples/cert/z3_hol_01 SMT/Examples/cert/z3_hol_01.proof \ |
|
1309 SMT/Examples/cert/z3_hol_02 SMT/Examples/cert/z3_hol_02.proof \ |
|
1310 SMT/Examples/cert/z3_hol_03 SMT/Examples/cert/z3_hol_03.proof \ |
|
1311 SMT/Examples/cert/z3_hol_04 SMT/Examples/cert/z3_hol_04.proof \ |
|
1312 SMT/Examples/cert/z3_hol_05 SMT/Examples/cert/z3_hol_05.proof \ |
|
1313 SMT/Examples/cert/z3_hol_06 SMT/Examples/cert/z3_hol_06.proof \ |
|
1314 SMT/Examples/cert/z3_hol_07 SMT/Examples/cert/z3_hol_07.proof \ |
|
1315 SMT/Examples/cert/z3_hol_08 SMT/Examples/cert/z3_hol_08.proof \ |
|
1316 SMT/Examples/cert/z3_linarith_01 \ |
|
1317 SMT/Examples/cert/z3_linarith_01.proof \ |
|
1318 SMT/Examples/cert/z3_linarith_02 \ |
|
1319 SMT/Examples/cert/z3_linarith_02.proof \ |
|
1320 SMT/Examples/cert/z3_linarith_03 \ |
|
1321 SMT/Examples/cert/z3_linarith_03.proof \ |
|
1322 SMT/Examples/cert/z3_linarith_04 \ |
|
1323 SMT/Examples/cert/z3_linarith_04.proof \ |
|
1324 SMT/Examples/cert/z3_linarith_05 \ |
|
1325 SMT/Examples/cert/z3_linarith_05.proof \ |
|
1326 SMT/Examples/cert/z3_linarith_06 \ |
|
1327 SMT/Examples/cert/z3_linarith_06.proof \ |
|
1328 SMT/Examples/cert/z3_linarith_07 \ |
|
1329 SMT/Examples/cert/z3_linarith_07.proof \ |
|
1330 SMT/Examples/cert/z3_linarith_08 \ |
|
1331 SMT/Examples/cert/z3_linarith_08.proof \ |
|
1332 SMT/Examples/cert/z3_linarith_09 \ |
|
1333 SMT/Examples/cert/z3_linarith_09.proof \ |
|
1334 SMT/Examples/cert/z3_linarith_10 \ |
|
1335 SMT/Examples/cert/z3_linarith_10.proof \ |
|
1336 SMT/Examples/cert/z3_linarith_11 \ |
|
1337 SMT/Examples/cert/z3_linarith_11.proof \ |
|
1338 SMT/Examples/cert/z3_linarith_12 \ |
|
1339 SMT/Examples/cert/z3_linarith_12.proof \ |
|
1340 SMT/Examples/cert/z3_linarith_13 \ |
|
1341 SMT/Examples/cert/z3_linarith_13.proof \ |
|
1342 SMT/Examples/cert/z3_linarith_14 \ |
|
1343 SMT/Examples/cert/z3_linarith_14.proof \ |
|
1344 SMT/Examples/cert/z3_linarith_15 \ |
|
1345 SMT/Examples/cert/z3_linarith_15.proof \ |
|
1346 SMT/Examples/cert/z3_linarith_16 \ |
|
1347 SMT/Examples/cert/z3_linarith_16.proof \ |
|
1348 SMT/Examples/cert/z3_linarith_17 \ |
|
1349 SMT/Examples/cert/z3_linarith_17.proof \ |
|
1350 SMT/Examples/cert/z3_linarith_18 \ |
|
1351 SMT/Examples/cert/z3_linarith_18.proof \ |
|
1352 SMT/Examples/cert/z3_linarith_19 \ |
|
1353 SMT/Examples/cert/z3_linarith_19.proof \ |
|
1354 SMT/Examples/cert/z3_linarith_20 \ |
|
1355 SMT/Examples/cert/z3_linarith_20.proof \ |
|
1356 SMT/Examples/cert/z3_linarith_21 \ |
|
1357 SMT/Examples/cert/z3_linarith_21.proof SMT/Examples/cert/z3_mono_01 \ |
|
1358 SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02 \ |
|
1359 SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01 \ |
|
1360 SMT/Examples/cert/z3_nat_arith_01.proof \ |
|
1361 SMT/Examples/cert/z3_nat_arith_02 \ |
|
1362 SMT/Examples/cert/z3_nat_arith_02.proof \ |
|
1363 SMT/Examples/cert/z3_nat_arith_03 \ |
|
1364 SMT/Examples/cert/z3_nat_arith_03.proof \ |
|
1365 SMT/Examples/cert/z3_nat_arith_04 \ |
|
1366 SMT/Examples/cert/z3_nat_arith_04.proof \ |
|
1367 SMT/Examples/cert/z3_nat_arith_05 \ |
|
1368 SMT/Examples/cert/z3_nat_arith_05.proof \ |
|
1369 SMT/Examples/cert/z3_nat_arith_06 \ |
|
1370 SMT/Examples/cert/z3_nat_arith_06.proof \ |
|
1371 SMT/Examples/cert/z3_nat_arith_07 \ |
|
1372 SMT/Examples/cert/z3_nat_arith_07.proof \ |
|
1373 SMT/Examples/cert/z3_nlarith_01 \ |
|
1374 SMT/Examples/cert/z3_nlarith_01.proof \ |
|
1375 SMT/Examples/cert/z3_nlarith_02 \ |
|
1376 SMT/Examples/cert/z3_nlarith_02.proof \ |
|
1377 SMT/Examples/cert/z3_nlarith_03 \ |
|
1378 SMT/Examples/cert/z3_nlarith_03.proof \ |
|
1379 SMT/Examples/cert/z3_nlarith_04 \ |
|
1380 SMT/Examples/cert/z3_nlarith_04.proof SMT/Examples/cert/z3_pair_01 \ |
|
1381 SMT/Examples/cert/z3_pair_01.proof SMT/Examples/cert/z3_pair_02 \ |
|
1382 SMT/Examples/cert/z3_pair_02.proof SMT/Examples/cert/z3_prop_01 \ |
|
1383 SMT/Examples/cert/z3_prop_01.proof SMT/Examples/cert/z3_prop_02 \ |
|
1384 SMT/Examples/cert/z3_prop_02.proof SMT/Examples/cert/z3_prop_03 \ |
|
1385 SMT/Examples/cert/z3_prop_03.proof SMT/Examples/cert/z3_prop_04 \ |
|
1386 SMT/Examples/cert/z3_prop_04.proof SMT/Examples/cert/z3_prop_05 \ |
|
1387 SMT/Examples/cert/z3_prop_05.proof SMT/Examples/cert/z3_prop_06 \ |
|
1388 SMT/Examples/cert/z3_prop_06.proof SMT/Examples/cert/z3_prop_07 \ |
|
1389 SMT/Examples/cert/z3_prop_07.proof SMT/Examples/cert/z3_prop_08 \ |
|
1390 SMT/Examples/cert/z3_prop_08.proof SMT/Examples/cert/z3_prop_09 \ |
|
1391 SMT/Examples/cert/z3_prop_09.proof SMT/Examples/cert/z3_prop_10 \ |
|
1392 SMT/Examples/cert/z3_prop_10.proof |
|
1393 @cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples |
1233 @cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples |
1394 |
1234 |
1395 |
1235 |
1396 ## HOL-Boogie |
1236 ## HOL-Boogie |
1397 |
1237 |