# HG changeset patch
# User paulson
# Date 929004057 -7200
# Node ID ac4c9707ae53cc189a29d526b6258ebd99334ab9
# Parent  4700ca722bbd5e11b642727acfed6a7f1bb6d4cd
moved predicates refl, sym down to Relation.thy

diff -r 4700ca722bbd -r ac4c9707ae53 src/HOL/Integ/Equiv.thy
--- a/src/HOL/Integ/Equiv.thy	Thu Jun 10 10:39:38 1999 +0200
+++ b/src/HOL/Integ/Equiv.thy	Thu Jun 10 10:40:57 1999 +0200
@@ -8,16 +8,13 @@
 
 Equiv = Relation + Finite + 
 consts
-    refl,equiv  ::      "['a set,('a*'a) set]=>bool"
-    sym         ::      "('a*'a) set=>bool"
-    "'/"        ::      "['a set,('a*'a) set]=>'a set set"  (infixl 90) 
-                        (*set of equiv classes*)
-    congruent   ::      "[('a*'a) set,'a=>'b]=>bool"
-    congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
+    equiv      :: "['a set, ('a*'a) set] => bool"
+    quotient   :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/" 90) 
+                         (*set of equiv classes*)
+    congruent  :: "[('a*'a) set, 'a=>'b] => bool"
+    congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool"
 
 defs
-    refl_def      "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
-    sym_def       "sym(r)    == ALL x y. (x,y): r --> (y,x): r"
     equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
     quotient_def  "A/r == UN x:A. {r^^{x}}"  
     congruent_def   "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"