src/ZF/func.thy
changeset 13221 e29378f347e4
parent 13219 7e44aa8a276e
child 13248 ae66c22ed52e
     1.1 --- a/src/ZF/func.thy	Tue Jun 18 18:45:07 2002 +0200
     1.2 +++ b/src/ZF/func.thy	Wed Jun 19 09:03:34 2002 +0200
     1.3 @@ -8,6 +8,13 @@
     1.4  
     1.5  theory func = equalities:
     1.6  
     1.7 +lemma relation_converse_converse [simp]:
     1.8 +     "relation(r) ==> converse(converse(r)) = r"
     1.9 +by (simp add: relation_def, blast) 
    1.10 +
    1.11 +lemma relation_restrict [simp]:  "relation(restrict(r,A))"
    1.12 +by (simp add: restrict_def relation_def, blast) 
    1.13 +
    1.14  (*** The Pi operator -- dependent function space ***)
    1.15  
    1.16  lemma Pi_iff: