changeset 1794 | e2b7ba2160f1 |
parent 1793 | 09fff2f0d727 |
child 1795 | 0466f9668ba3 |
--- a/src/HOL/ex/Rec.thy Thu Jun 13 16:22:37 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -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