src/HOL/Arith.ML
changeset 5771 7c2c8cf20221
parent 5758 27a2b36efd95
child 5983 79e301a6a51b
     1.1 --- a/src/HOL/Arith.ML	Mon Oct 26 13:05:08 1998 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Oct 28 11:25:38 1998 +0100
     1.3 @@ -435,11 +435,6 @@
     1.4  qed "diff_is_0_eq";
     1.5  Addsimps [diff_is_0_eq RS iffD2];
     1.6  
     1.7 -Goal "m-n = 0  -->  n-m = 0  -->  m=n";
     1.8 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
     1.9 -by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
    1.10 -qed_spec_mp "diffs0_imp_equal";
    1.11 -
    1.12  Goal "(0<n-m) = (m<n)";
    1.13  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.14  by (ALLGOALS Asm_simp_tac);