# HG changeset patch
# User paulson
# Date 834137797 -7200
# Node ID 6b38717439c67c9de65c9c89384e3d4618e497ae
# Parent  2f3694c50101e7e79d6345b9920bb7e9034493e4
Addition of converse_iff, domain_converse, range_converse as rewrites

diff -r 2f3694c50101 -r 6b38717439c6 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Thu Jun 06 16:20:27 1996 +0200
+++ b/src/ZF/Cardinal.ML	Fri Jun 07 10:56:37 1996 +0200
@@ -744,8 +744,7 @@
 by (etac nat_induct 1);
 by (fast_tac (ZF_cs addIs [wf_onI]) 1);
 by (rtac wf_onI 1);
-by (asm_full_simp_tac
-    (ZF_ss addsimps [wf_on_def, wf_def, converse_iff, Memrel_iff]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [wf_on_def, wf_def, Memrel_iff]) 1);
 by (excluded_middle_tac "x:Z" 1);
 by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2);
 by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [mem_asym]) 2);
diff -r 2f3694c50101 -r 6b38717439c6 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Jun 06 16:20:27 1996 +0200
+++ b/src/ZF/Order.ML	Fri Jun 07 10:56:37 1996 +0200
@@ -515,8 +515,7 @@
 by (rtac well_ord_mono_ord_isoI 1);
 by (resolve_tac [converse_ord_iso_map RS subst] 4);
 by (asm_simp_tac 
-    (ZF_ss addsimps [ord_iso_map_subset RS converse_converse, 
-                     domain_converse, range_converse]) 4);
+    (ZF_ss addsimps [ord_iso_map_subset RS converse_converse]) 4);
 by (REPEAT (ares_tac [ord_iso_map_mono_map] 3));
 by (ALLGOALS (etac well_ord_subset));
 by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map]));
diff -r 2f3694c50101 -r 6b38717439c6 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Thu Jun 06 16:20:27 1996 +0200
+++ b/src/ZF/Perm.ML	Fri Jun 07 10:56:37 1996 +0200
@@ -156,9 +156,7 @@
 (*** Converse of a function ***)
 
 goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) : range(f)->A";
-by (asm_simp_tac 
-    (ZF_ss addsimps [Pi_iff, function_def, 
-		     domain_converse, converse_iff]) 1);
+by (asm_simp_tac (ZF_ss addsimps [Pi_iff, function_def]) 1);
 by (eresolve_tac [CollectE] 1);
 by (asm_simp_tac (ZF_ss addsimps [apply_iff]) 1);
 by (fast_tac (ZF_cs addDs [fun_is_rel]) 1);
diff -r 2f3694c50101 -r 6b38717439c6 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Jun 06 16:20:27 1996 +0200
+++ b/src/ZF/simpdata.ML	Fri Jun 07 10:56:37 1996 +0200
@@ -75,6 +75,7 @@
      succI1, succ_not_0, succ_not_0 RS not_sym, succ_inject_iff,
      ball_simp, if_true, if_false, 
      beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
+     converse_iff, domain_converse, range_converse,
      Sigma_empty1, Sigma_empty2, triv_RepFun, subset_refl];
 
 (*Sigma_cong, Pi_cong NOT included by default since they cause