equal
deleted
inserted
replaced
67 qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod(p,p)" |
67 qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod(p,p)" |
68 (fn prems => |
68 (fn prems => |
69 [ |
69 [ |
70 (res_inst_tac [("p","p")] PairE 1), |
70 (res_inst_tac [("p","p")] PairE 1), |
71 (hyp_subst_tac 1), |
71 (hyp_subst_tac 1), |
72 (simp_tac pair_ss 1), |
72 (simp_tac prod_ss 1), |
73 (simp_tac Cfun_ss 1) |
73 (simp_tac Cfun_ss 1) |
74 ]); |
74 ]); |
75 |
75 |
76 qed_goal "antisym_less_cprod" Cprod1.thy |
76 qed_goal "antisym_less_cprod" Cprod1.thy |
77 "[|less_cprod(p1,p2);less_cprod(p2,p1)|] ==> p1=p2" |
77 "[|less_cprod(p1,p2);less_cprod(p2,p1)|] ==> p1=p2" |
103 (res_inst_tac [("p","p2")] PairE 1), |
103 (res_inst_tac [("p","p2")] PairE 1), |
104 (hyp_subst_tac 1), |
104 (hyp_subst_tac 1), |
105 (dtac less_cprod2c 1), |
105 (dtac less_cprod2c 1), |
106 (dtac less_cprod2c 1), |
106 (dtac less_cprod2c 1), |
107 (rtac (less_cprod1b RS ssubst) 1), |
107 (rtac (less_cprod1b RS ssubst) 1), |
108 (simp_tac pair_ss 1), |
108 (simp_tac prod_ss 1), |
109 (etac conjE 1), |
109 (etac conjE 1), |
110 (etac conjE 1), |
110 (etac conjE 1), |
111 (rtac conjI 1), |
111 (rtac conjI 1), |
112 (etac trans_less 1), |
112 (etac trans_less 1), |
113 (atac 1), |
113 (atac 1), |