Theory Names

Up to index of Isabelle/HOL/PI

theory Names = InfClass:
(* Title:    Names.thy
   Author:   Christine Roeckl

Free names in names abstractions.
*)

Names = InfClass +

(* free names *)
constdefs
  fnna :: (('a::inf_class) => 'a) => 'a set
 "fnna fa == {a. ALL b. fa b = a}"

  fnnaa :: (('a::inf_class) => 'a => 'a) => 'a set
 "fnnaa ffa == {a. ALL b c. ffa b c = a}"

(* substitution of names *)
constdefs
  nsubst :: ('a::inf_class) => 'a => 'a => 'a
 "nsubst c d a == if a=c then d else a"

end