--- a/Gfp.thy Thu Nov 24 20:11:40 1994 +0100
+++ b/Gfp.thy Thu Nov 24 20:31:09 1994 +0100
@@ -8,7 +8,7 @@
Gfp = Lfp +
consts gfp :: "['a set=>'a set] => 'a set"
-rules
+defs
(*greatest fixed point*)
gfp_def "gfp(f) == Union({u. u <= f(u)})"
end
--- a/Lfp.thy Thu Nov 24 20:11:40 1994 +0100
+++ b/Lfp.thy Thu Nov 24 20:31:09 1994 +0100
@@ -8,7 +8,7 @@
Lfp = mono +
consts lfp :: "['a set=>'a set] => 'a set"
-rules
+defs
(*least fixed point*)
lfp_def "lfp(f) == Inter({u. f(u) <= u})"
end
--- a/Sexp.thy Thu Nov 24 20:11:40 1994 +0100
+++ b/Sexp.thy Thu Nov 24 20:31:09 1994 +0100
@@ -24,7 +24,7 @@
NumbI "Numb(a): sexp"
SconsI "[| M: sexp; N: sexp |] ==> M$N : sexp"
-rules
+defs
sexp_case_def
"sexp_case(c,d,e,M) == @ z. (? x. M=Leaf(x) & z=c(x)) \
@@ -38,4 +38,3 @@
"sexp_rec(M,c,d,e) == wfrec(pred_sexp, M, \
\ %M g. sexp_case(c, d, %N1 N2. e(N1, N2, g(N1), g(N2)), M))"
end
-
--- a/Trancl.thy Thu Nov 24 20:11:40 1994 +0100
+++ b/Trancl.thy Thu Nov 24 20:31:09 1994 +0100
@@ -15,7 +15,7 @@
rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
-rules
+defs
trans_def "trans(r) == (!x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
comp_def (*composition of relations*)
"r O s == {xz. ? x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
--- a/WF.thy Thu Nov 24 20:11:40 1994 +0100
+++ b/WF.thy Thu Nov 24 20:31:09 1994 +0100
@@ -14,7 +14,7 @@
is_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b, 'a=>'b] => bool"
the_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
-rules
+defs
wf_def "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
cut_def "cut(f,r,x) == (%y. if(<y,x>:r, f(y), @z.True))"