# HG changeset patch
# User nipkow
# Date 785705469 -3600
# Node ID 12dd5d2e266b1fbb273826ed2b5eb8f850c294ad
# Parent  768d3504d7cdec30395c93473e03b7daa0610bc7
rules -> defs

diff -r 768d3504d7cd -r 12dd5d2e266b Gfp.thy
--- 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
diff -r 768d3504d7cd -r 12dd5d2e266b Lfp.thy
--- 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
diff -r 768d3504d7cd -r 12dd5d2e266b Sexp.thy
--- 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
-
diff -r 768d3504d7cd -r 12dd5d2e266b Trancl.thy
--- 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}"
diff -r 768d3504d7cd -r 12dd5d2e266b WF.thy
--- 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))"