| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Metis_Examples/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 505 B |
|
Quelle Sledgehammer_Isar_Proofs.thy Sprache: Isabelle |
|||||||||||||||
|
(* Title: src/HOL/Metis_Example/Sledgehammer_Isar_Proofs.thy Author: Martin Desharnais, MPI-INF Saarbruecken Tests of proof reconstruction (a.k.a. preplay) in Sledgehammer. *) theory Sledgehammer_Isar_Proofs imports Main begin external_file ‹Sledgehammer_Isar_Proofs.certs› declare [[smt_certificates = "Sledgehammer_Isar_Proofs.certs"]] declare [[smt_read_only_certificates = true]] sledgehammer_params [verit, isar_proof, minimize = false, slices = 1, compress = 1] end
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-09-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-10