| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Pure/ex/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 601 B |
|
Quelle Def_Examples.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Pure/ex/Def_Examples.thy Author: Makarius Some examples for primitive definitions. *) theory Def_Examples imports Def begin section ‹Global definitions› def "I x ≡ x" def "K x y ≡ x" def "S x y z ≡ (x z) (y z)" lemma "I (I x) ≡ x" by simp lemma "K a x ≡ K a y" by simp lemma "S K K ≡ I" by simp section ‹Locale definitions› locale const = fixes a :: 'a begin def "fun b ≡ a" lemma "fun x ≡ fun y" by simp end lemma "const.fun a x ≡ const.fun a y" by simp end
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09