| author | haftmann |
| Thu, 19 Jun 2025 17:15:40 +0200 | |
| changeset 82734 | 89347c0cc6a3 |
| parent 78745 | f9c559d33ff3 |
| permissions | -rw-r--r-- |
|
78676
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
1 |
(* Title: src/HOL/Metis_Example/Sledgehammer_Isar_Proofs.thy |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
2 |
Author: Martin Desharnais, MPI-INF Saarbruecken |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
3 |
|
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
4 |
Tests of proof reconstruction (a.k.a. preplay) in Sledgehammer. |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
5 |
*) |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
6 |
theory Sledgehammer_Isar_Proofs |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
7 |
imports Main |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
8 |
begin |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
9 |
|
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
10 |
external_file \<open>Sledgehammer_Isar_Proofs.certs\<close> |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
11 |
declare [[smt_certificates = "Sledgehammer_Isar_Proofs.certs"]] |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
12 |
declare [[smt_read_only_certificates = true]] |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
13 |
|
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
14 |
sledgehammer_params [verit, isar_proof, minimize = false, slices = 1, compress = 1] |
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
15 |
|
|
a98e0a816d28
added first proof reconstruction test for Sledgehammer
desharna
parents:
diff
changeset
|
16 |
end |