--- a/src/ZF/Trancl.thy Thu Apr 22 11:02:22 2004 +0200
+++ b/src/ZF/Trancl.thy Thu Apr 22 12:11:17 2004 +0200
@@ -16,9 +16,6 @@
irrefl :: "[i,i]=>o"
"irrefl(A,r) == ALL x: A. <x,x> ~: r"
- equiv :: "[i,i]=>o"
- "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
-
sym :: "i=>o"
"sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
@@ -41,6 +38,10 @@
trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
"r^+ == r O r^*"
+ equiv :: "[i,i]=>o"
+ "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
+
+
subsection{*General properties of relations*}
subsubsection{*irreflexivity*}