| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/LightweightJava/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 1 kB |
|
SSL Closure_Set.thySprache: 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.7 Sekunden (vorverarbeitet am 2026-06-10) ¤*Bot Zugriff |
|
||||||||||||||
2026-06-09