equal
deleted
inserted
replaced
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 |
68 |
68 |
69 qed_goal " monofun_Ispair" Sprod2.thy |
69 qed_goal "monofun_Ispair" Sprod2.thy |
70 "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2" |
70 "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2" |
71 (fn prems => |
71 (fn prems => |
72 [ |
72 [ |
73 (cut_facts_tac prems 1), |
73 (cut_facts_tac prems 1), |
74 (rtac trans_less 1), |
74 (rtac trans_less 1), |