equal
deleted
inserted
replaced
114 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
114 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
115 by (cut_facts_tac [linorder_linear] 1); |
115 by (cut_facts_tac [linorder_linear] 1); |
116 by (Blast_tac 1); |
116 by (Blast_tac 1); |
117 qed "linorder_less_linear"; |
117 qed "linorder_less_linear"; |
118 |
118 |
|
119 val prems = goal thy |
|
120 "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P"; |
|
121 by(cut_facts_tac [linorder_less_linear] 1); |
|
122 by(REPEAT(eresolve_tac (prems@[disjE]) 1)); |
|
123 qed "linorder_less_split"; |
|
124 |
119 Goal "!!x::'a::linorder. (~ x < y) = (y <= x)"; |
125 Goal "!!x::'a::linorder. (~ x < y) = (y <= x)"; |
120 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
126 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
121 by (cut_facts_tac [linorder_linear] 1); |
127 by (cut_facts_tac [linorder_linear] 1); |
122 by (blast_tac (claset() addIs [order_antisym]) 1); |
128 by (blast_tac (claset() addIs [order_antisym]) 1); |
123 qed "linorder_not_less"; |
129 qed "linorder_not_less"; |