# HG changeset patch
# User lcp
# Date 786065491 -3600
# Node ID ec86863e87c8f0f2b44e6cd26d7b2d96b5a67468
# Parent  b89462f9d5f1895db56b35540d8f1b79665420e4
replaced "rules" by "defs"

diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Arith.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
     "#+" :: "[i,i]=>i"      		(infixl 65)
     "#-" :: "[i,i]=>i"      		(infixl 65)
 
-rules
+defs
     rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
 
     add_def  "m#+n == rec(m, n, %u v.succ(v))"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Bool.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -19,7 +19,7 @@
 translations
    "1"  == "succ(0)"
 
-rules
+defs
     bool_def	"bool == {0,1}"
     cond_def	"cond(b,c,d) == if(b=1,c,d)"
     not_def	"not(b) == cond(b,0,1)"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Cardinal.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
 
   swap       :: "[i,i,i]=>i"     (*not used; useful??*)
 
-rules
+defs
 
   (*least ordinal operator*)
   Least_def  "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/CardinalArith.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -16,7 +16,7 @@
   jump_cardinal :: "i=>i"
   csucc       :: "i=>i"
 
-rules
+defs
 
   InfCard_def  "InfCard(i) == Card(i) & nat le i"
 
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Epsilon.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
     eclose,rank ::      "i=>i"
     transrec    ::      "[i, [i,i]=>i] =>i"
 
-rules
+defs
   eclose_def	"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
   transrec_def	"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
   rank_def    	"rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/EquivClass.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
     congruent	::	"[i,i=>i]=>o"
     congruent2  ::      "[i,[i,i]=>i]=>o"
 
-rules
+defs
     quotient_def  "A/r == {r``{x} . x:A}"
     congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
 
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Fixedpt.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
   bnd_mono    :: "[i,i=>i]=>o"
   lfp, gfp    :: "[i,i=>i]=>i"
 
-rules
+defs
   (*monotone operator from Pow(D) to itself*)
   bnd_mono_def 
       "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/IMP/Com.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -96,7 +96,7 @@
 translations
        "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
 
-rules 
+defs 
 	assign_def	"sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
 
 inductive
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/IMP/Denotation.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -14,7 +14,7 @@
   C     :: "i => i"
   Gamma :: "[i,i,i] => i"
 
-rules
+rules	(*NOT definitional*)
   A_nat_def	"A(N(n)) == (%sigma. n)"
   A_loc_def	"A(X(x)) == (%sigma. sigma`x)" 
   A_op1_def	"A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/List.thy
--- a/src/ZF/List.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/List.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -39,7 +39,7 @@
   "[]"          == "Nil"
 
 
-rules
+defs
 
   hd_def	"hd(l)	     == list_case(0, %x xs.x, l)"
   tl_def	"tl(l)       == list_case(Nil, %x xs.xs, l)"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Nat.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
     nat_case    ::      "[i, i=>i, i]=>i"
     nat_rec     ::      "[i, i, [i,i]=>i]=>i"
 
-rules
+defs
 
     nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
 
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/OrderArith.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
   radd, rmult      :: "[i,i,i,i]=>i"
   rvimage          :: "[i,i,i]=>i"
 
-rules
+defs
   (*disjoint sum of two relations; underlies ordinal addition*)
   radd_def "radd(A,r,B,s) == \
 \                {z: (A+B) * (A+B).  \
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/OrderType.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -13,7 +13,7 @@
   ordermap  :: "[i,i]=>i"
   ordertype :: "[i,i]=>i"
 
-rules
+defs
   ordermap_def
       "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
 
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Ordinal.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -17,12 +17,11 @@
 translations
   "x le y"      == "x < succ(y)"
 
-rules
+defs
   Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   Transset_def	"Transset(i) == ALL x:i. x<=i"
   Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
   lt_def        "i<j         == i:j & Ord(j)"
   Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
 
-
 end
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Perm.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -15,7 +15,7 @@
     id  	::      "i=>i"
     inj,surj,bij::      "[i,i]=>i"
 
-rules
+defs
 
     (*composition of relations and functions; NOT Suppes's relative product*)
     comp_def	"r O s == {xz : domain(s)*range(r) . \
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/QPair.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -29,7 +29,7 @@
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
   "A <*> B"      => "QSigma(A, _K(B))"
 
-rules
+defs
   QPair_def       "<a;b> == a+b"
   qsplit_def      "qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)"
   qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/QUniv.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -10,7 +10,7 @@
 consts
     quniv        :: "i=>i"
 
-rules
+defs
     quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
 
 end
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Rel.thy
--- a/src/ZF/Rel.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Rel.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
     sym,asym,antisym,trans :: "i=>o"
     trans_on               :: "[i,i]=>o"	("trans[_]'(_')")
 
-rules
+defs
   refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
 
   irrefl_def   "irrefl(A,r) == ALL x: A. <x,x> ~: r"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Sum.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -14,7 +14,7 @@
     case        :: "[i=>i, i=>i, i]=>i"
     Part        :: "[i,i=>i] => i"
 
-rules
+defs
     sum_def     "A+B == {0}*A Un {1}*B"
     Inl_def     "Inl(a) == <0,a>"
     Inr_def     "Inr(b) == <1,b>"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Trancl.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
     rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
     trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
 
-rules
+defs
     rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
     trancl_def  "r^+ == r O r^*"
 end
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Univ.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -21,7 +21,7 @@
 translations
     "Vset(x)"   == 	"Vfrom(0,x)"
 
-rules
+defs
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
 
     Vrec_def
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Zorn.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -19,7 +19,7 @@
   chain, maxchain :: "i=>i"
   super           :: "[i,i]=>i"
 
-rules
+defs
   Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
   increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
 
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/BT.thy
--- a/src/ZF/ex/BT.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/BT.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -18,7 +18,7 @@
 datatype
   "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
   
-rules
+defs
   bt_rec_def
     "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
 
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/Bin.thy
--- a/src/ZF/ex/Bin.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Bin.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -23,7 +23,7 @@
         | "$$" ("w: bin", "b: bool")    (infixl 60)
   type_intrs "[bool_into_univ]"
   
-rules
+defs
 
   bin_rec_def
       "bin_rec(z,a,b,h) == \
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/Comb.thy
--- a/src/ZF/ex/Comb.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Comb.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -71,7 +71,7 @@
   diamond   :: "i => o"
   I         :: "i"
 
-rules
+defs
 
   diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
 \                            (ALL y'. <x,y'>:r --> \
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/Integ.thy
--- a/src/ZF/ex/Integ.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Integ.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -20,7 +20,7 @@
     "$-"        ::      "[i,i]=>i"      (infixl 65)
     "$<"	:: 	"[i,i]=>o"  	(infixl 50)
 
-rules
+defs
 
     intrel_def
      "intrel == {p:(nat*nat)*(nat*nat). 		\
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/LList.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -43,9 +43,10 @@
   lconst   :: "i => i"
   flip     :: "i => i"
 
-rules
+defs
   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
 
+rules
   flip_LNil   "flip(LNil) = LNil"
 
   flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/Primrec.thy
--- a/src/ZF/ex/Primrec.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Primrec.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -28,7 +28,7 @@
 translations
   "ack(x,y)"  == "ACK(x) ` [y]"
 
-rules
+defs
 
   SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
 
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/PropLog.thy
--- a/src/ZF/ex/PropLog.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/PropLog.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -44,7 +44,7 @@
   "|="     :: "[i,i] => o"    			(infixl 50)
   hyps     :: "[i,i] => i"
 
-rules
+defs
 
   prop_rec_def
    "prop_rec(p,b,c,h) == \
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Ramsey.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -24,7 +24,7 @@
   Atleast     		:: "[i,i]=>o"
   Clique,Indept,Ramsey	:: "[i,i,i]=>o"
 
-rules
+defs
 
   Symmetric_def
     "Symmetric(E) == (ALL x y. <x,y>:E --> <y,x>:E)"
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/TF.thy
--- a/src/ZF/ex/TF.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/TF.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -22,7 +22,7 @@
 and
   "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
 
-rules
+defs
   TF_rec_def
     "TF_rec(z,b,c,d) == Vrec(z,  			\
 \      %z r. tree_forest_case(%x f. b(x, f, r`f), 	\
diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/Term.thy
--- a/src/ZF/ex/Term.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Term.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -26,7 +26,7 @@
     type_intrs  "[list_univ RS subsetD]"
 *)
 
-rules
+defs
   term_rec_def
    "term_rec(t,d) == \
 \   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"