equal
deleted
inserted
replaced
66 by (dres_inst_tac [("P","~x<y")] conjE 1); |
66 by (dres_inst_tac [("P","~x<y")] conjE 1); |
67 by (assume_tac 2); |
67 by (assume_tac 2); |
68 by (rtac (Suc_diff_n RS sym) 1); |
68 by (rtac (Suc_diff_n RS sym) 1); |
69 by (rtac le_less_trans 1); |
69 by (rtac le_less_trans 1); |
70 by (etac (not_less_eq RS subst) 2); |
70 by (etac (not_less_eq RS subst) 2); |
71 by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1); |
71 by (rtac (hd ([diff_less_Suc RS Suc_leI] RL [Suc_le_mono RS subst])) 1); |
72 qed "diff_add_not_assoc"; |
72 qed "diff_add_not_assoc"; |
73 |
73 |
74 val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)"; |
74 val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)"; |
75 by (cut_facts_tac prems 1); |
75 by (cut_facts_tac prems 1); |
76 by (rtac mp 1); |
76 by (rtac mp 1); |