src/ZF/func.thy

--- a/src/ZF/func.thy	Tue Jun 18 18:45:07 2002 +0200
+++ b/src/ZF/func.thy	Wed Jun 19 09:03:34 2002 +0200
@@ -8,6 +8,13 @@
 
 theory func = equalities:
 
+lemma relation_converse_converse [simp]:
+     "relation(r) ==> converse(converse(r)) = r"
+by (simp add: relation_def, blast) 
+
+lemma relation_restrict [simp]:  "relation(restrict(r,A))"
+by (simp add: restrict_def relation_def, blast) 
+
 (*** The Pi operator -- dependent function space ***)
 
 lemma Pi_iff: