equal
deleted
inserted
replaced
45 (strip_tac 1), |
45 (strip_tac 1), |
46 (rtac (less_fun RS iffD2) 1), |
46 (rtac (less_fun RS iffD2) 1), |
47 (strip_tac 1), |
47 (strip_tac 1), |
48 (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), |
48 (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), |
49 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
49 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
50 (forward_tac [notUU_I] 1), |
50 (ftac notUU_I 1), |
51 (atac 1), |
51 (atac 1), |
52 (REPEAT(asm_simp_tac(Sprod0_ss |
52 (REPEAT(asm_simp_tac(Sprod0_ss |
53 addsimps[inst_sprod_po,refl_less,minimal]) 1)) |
53 addsimps[inst_sprod_po,refl_less,minimal]) 1)) |
54 ]); |
54 ]); |
55 |
55 |
57 (fn prems => |
57 (fn prems => |
58 [ |
58 [ |
59 (strip_tac 1), |
59 (strip_tac 1), |
60 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
60 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
61 (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), |
61 (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), |
62 (forward_tac [notUU_I] 1), |
62 (ftac notUU_I 1), |
63 (atac 1), |
63 (atac 1), |
64 (REPEAT(asm_simp_tac(Sprod0_ss |
64 (REPEAT(asm_simp_tac(Sprod0_ss |
65 addsimps[inst_sprod_po,refl_less,minimal]) 1)) |
65 addsimps[inst_sprod_po,refl_less,minimal]) 1)) |
66 ]); |
66 ]); |
67 |
67 |