| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Mirabelle.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/Mirabelle.thy Author: Jasmin Blanchette, TU Munich Author: Sascha Boehme, TU Munich Author: Makarius Author: Martin Desharnais, UniBw Munich, MPI-INF Saarbrücken *) theory Mirabelle imports Sledgehammer Predicate_Compile Presburger begin ML_file ‹Tools/Mirabelle/mirabelle_util.ML› ML_file ‹Tools/Mirabelle/mirabelle.ML› ML ‹ signature MIRABELLE_ACTION = sig val make_action : Mirabelle.action_context -> string * Mirabelle.action end › ML_file ‹Tools/Mirabelle/mirabelle_arith.ML› ML_file ‹Tools/Mirabelle/mirabelle_order.ML› ML_file ‹Tools/Mirabelle/mirabelle_metis.ML› ML_file ‹Tools/Mirabelle/mirabelle_presburger.ML› ML_file ‹Tools/Mirabelle/mirabelle_quickcheck.ML› ML_file ‹Tools/Mirabelle/mirabelle_sledgehammer_filter.ML› ML_file ‹Tools/Mirabelle/mirabelle_sledgehammer.ML› ML_file ‹Tools/Mirabelle/mirabelle_try0.ML› end
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26