equal
deleted
inserted
replaced
256 end |
256 end |
257 end |
257 end |
258 |
258 |
259 val canonical_isar_supported_prover = eN |
259 val canonical_isar_supported_prover = eN |
260 val z3N = "z3" |
260 val z3N = "z3" |
261 val veriT_newN = "veriT" |
|
262 |
261 |
263 fun isar_supported_prover_of thy name = |
262 fun isar_supported_prover_of thy name = |
264 if is_atp thy name orelse name = z3N then name |
263 if is_atp thy name orelse name = z3N then name |
265 else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover |
264 else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover |
266 else name |
265 else name |