| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Containers/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 577 B |
|
Quelle Closure_Set.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* Title: Containers/Closure_set.thy Author: Andreas Lochbihler, KIT *) theory Closure_Set imports Equal begin section ‹Sets implemented as Closures› context equal_base begin definition fun_upd :: "('a → 'b) → 'a → 'b → 'a → 'b" where fun_upd_apply: "fun_upd f a b a' = (if equal a a' then b else f a')" end lemmas [code] = equal_base.fun_upd_apply lemmas [simp] = equal_base.fun_upd_apply lemma fun_upd_conv_fun_upd: "equal_base.fun_upd (=) = fun_upd" by(simp add: fun_eq_iff) end
¤ Dauer der Verarbeitung: 0.2 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01