| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Kleene_Algebra/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 644 B |
|
Quelle PHL_DRA.thySprache: Isabelle |
|||||||||||||||
|
(* Title: General Hoare Logic for Demonic Refinement Algebra Author: Georg Struth Maintainer: Georg Struth <g.struth at sheffield.ac.uk> Tjark Weber <tjark.weber at it.uu.se> *) section ‹Propositional Hoare Logic for Demonic Refinement Algebra› text ‹In this section the generic iteration operator is instantiated to the stron refinement algebra that models possibly infinite iteration. theory PHL_DRA imports DRA PHL_KA begin sublocale dra < total_phl: it_pre_dioid where it = strong_iteration by standard (simp add: local.iteration_sim) end
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09