src/ZF/UNITY/UNITY.ML
changeset 13176 312bd350579b
parent 12537 f2cda6fb1c9f
child 13612 55d32e76ef4e
--- a/src/ZF/UNITY/UNITY.ML	Thu May 23 17:05:21 2002 +0200
+++ b/src/ZF/UNITY/UNITY.ML	Fri May 24 13:15:37 2002 +0200
@@ -722,6 +722,7 @@
 by (cut_inst_tac [("F", "xa")] Acts_type 1);
 by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1);
 by Auto_tac;
+by (rename_tac "xa xc xd act xe xf" 1);
 by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); 
 by (dres_inst_tac [("x", "f`xf")] bspec 1);
 by Auto_tac;