| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/LTL/example/ (Archive of formal Proofs Version 2026-5©) Datei vom 31.4.2026 mit Größe 816 B |
|
Quelle Example.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* Author: Salomon Sickert License: BSD *) section ‹Example› theory Example imports "../LTL" "../Rewriting" "HOL-Library.Code_Target_Numeral" begin ― ‹The included parser always returns a @{typ "String.literal ltlc"}. If a differ is needed one can use @{const map_ltlc} to relabel the leafs. In our example we string to each atom. definition rewrite :: "String.literal ltlc → String.literal ltlc" where "rewrite ≡ ltln_to_ltlc o rewrite_iter_slow o ltlc_to_ltln o (map_ltlc (λs. Strin ― ‹Export rewriting engine (and also constructors)› export_code truec Iff_ltlc rewrite in SML file_prefix ‹rewrite_example› end
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01