ex/Rec.thy
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 0 7949f97df77a
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity

Rec = Fixedpt +
consts
fix	:: "('a=>'a) => 'a"
Dom	:: "(('a=>'b) => ('a=>'b)) => 'a set"
Domf	:: "(('a=>'b) => ('a=>'b)) => 'a set => 'a set"
rules
Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
Dom_def  "Dom(F) == lfp(Domf(F))"
end