# HG changeset patch
# User lcp
# Date 787915164 -3600
# Node ID 9bac814082e4fec037b38a52973ebf2ebf10ff47
# Parent  91c68f74f4585b7f2a6ec9ac97e23e2d8f5cd95e
Used bind_thm to store domain_rel_subset and range_rel_subset

diff -r 91c68f74f458 -r 9bac814082e4 src/ZF/mono.ML
--- a/src/ZF/mono.ML	Mon Dec 19 15:30:30 1994 +0100
+++ b/src/ZF/mono.ML	Tue Dec 20 10:19:24 1994 +0100
@@ -109,15 +109,13 @@
 by (fast_tac ZF_cs 1);
 qed "domain_mono";
 
-val domain_rel_subset = 
-	[domain_mono, domain_subset] MRS subset_trans |> standard;
+bind_thm ("domain_rel_subset", [domain_mono, domain_subset] MRS subset_trans);
 
 goal ZF.thy "!!r s. r<=s ==> range(r)<=range(s)";
 by (fast_tac ZF_cs 1);
 qed "range_mono";
 
-val range_rel_subset = 
-	[range_mono, range_subset] MRS subset_trans |> standard;
+bind_thm ("range_rel_subset", [range_mono, range_subset] MRS subset_trans);
 
 goal ZF.thy "!!r s. r<=s ==> field(r)<=field(s)";
 by (fast_tac ZF_cs 1);