changeset 13176 | 312bd350579b |
parent 12484 | 7ad150f5fc10 |
child 14046 | 6616e6c53d48 |
--- a/src/ZF/UNITY/Constrains.ML Thu May 23 17:05:21 2002 +0200 +++ b/src/ZF/UNITY/Constrains.ML Fri May 24 13:15:37 2002 +0200 @@ -470,6 +470,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;