equal
deleted
inserted
replaced
720 by (etac not_emptyE 1); |
720 by (etac not_emptyE 1); |
721 by (Clarify_tac 1); |
721 by (Clarify_tac 1); |
722 by (cut_inst_tac [("F", "xa")] Acts_type 1); |
722 by (cut_inst_tac [("F", "xa")] Acts_type 1); |
723 by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1); |
723 by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1); |
724 by Auto_tac; |
724 by Auto_tac; |
|
725 by (rename_tac "xa xc xd act xe xf" 1); |
725 by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); |
726 by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); |
726 by (dres_inst_tac [("x", "f`xf")] bspec 1); |
727 by (dres_inst_tac [("x", "f`xf")] bspec 1); |
727 by Auto_tac; |
728 by Auto_tac; |
728 by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); |
729 by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); |
729 by (dres_inst_tac [("x", "act")] bspec 1); |
730 by (dres_inst_tac [("x", "act")] bspec 1); |