Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Library/   (Firefox Browser Version 153.0.1©)  Datei vom 16.11.2025 mit Größe 6 kB image not shown  

SSL Mirabelle.thy   Sprache: 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 ‹
  MIRABELLE_ACTION = sig
 val make_action : Mirabelle.action_context -> string * Mirabelle.action
 
 ›

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

Messung V0.5 in Prozent
C=49 H=100 G=78

¤ Dauer der Verarbeitung: 0.12 Sekunden  (vorverarbeitet am  2026-09-28) ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders