(* 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
| Messung V0.5 in Prozent |
|---|
| | | |
[0.14QuellennavigatorsProjekt 2026-09-29]
