HOL/Makefile: now test depends upon SUBST_FILES
HOL/Makefile/SUBST_FILES: changed some filenames to upper case
HOL/Makefile: now executes ex/ROOT.ML after Subst/ROOT.ML
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