theory Ex
  imports FOL
begin

term "(\<lambda>y x. x = y)(x)"  (*"\<lambda>xa. xa = x"*)
term "(\<lambda>x y. y = x)(y)"  (*"\<lambda>ya. ya = y"*)

term True  (*constant "True"*)

locale loc =
  fixes x :: "'a" (structure)
    and y :: "'a" ("Y")
    and True :: o
begin

term "(\<lambda>y x. x = y)(x)"  (*"\<lambda>xa. xa = x"*)
term "(\<lambda>x y. y = x)(y)"  (*"\<lambda>ya. ya = Y"*)

term True  (*free "True"*)
thm TrueI  (*constant "IFOL.True"*)

end

notepad
begin
  fix x :: "'a" (structure)
  and y :: "'a" ("Y")
  and True :: o

  term "(\<lambda>y x. x = y)(x)"  (*"\<lambda>xa. xa = x"*)
  term "(\<lambda>x y. y = x)(y)"  (*"\<lambda>ya. ya = Y"*)

  term True  (*skolem "True"*)
  thm TrueI  (*constant "IFOL.True"*)
end

end