--- a/src/ZF/ZF.thy Tue Mar 13 12:04:07 2012 +0000
+++ b/src/ZF/ZF.thy Tue Mar 13 17:11:49 2012 +0000
@@ -406,6 +406,9 @@
apply (rule iff_refl)
done
+text{*For calculations*}
+declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
+
subsection{*Rules for equality*}