src/HOL/Divides.ML
changeset 11464 ddea204de5bc
parent 11396 48fc0db9b896
child 11593 ab08d61966b1
     1.1 --- a/src/HOL/Divides.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Divides.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4  by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
     1.5  qed "mod_if";
     1.6  
     1.7 -Goal "m mod 1 = (0::nat)";
     1.8 +Goal "m mod 1' = 0";
     1.9  by (induct_tac "m" 1);
    1.10  by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
    1.11  qed "mod_1";
    1.12 @@ -387,7 +387,7 @@
    1.13  
    1.14  (*** Further facts about div and mod ***)
    1.15  
    1.16 -Goal "m div 1 = m";
    1.17 +Goal "m div 1' = m";
    1.18  by (induct_tac "m" 1);
    1.19  by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
    1.20  qed "div_1";
    1.21 @@ -527,12 +527,12 @@
    1.22  qed "dvd_0_left_iff";
    1.23  AddIffs [dvd_0_left_iff];
    1.24  
    1.25 -Goalw [dvd_def] "1 dvd (k::nat)";
    1.26 +Goalw [dvd_def] "1' dvd k";
    1.27  by (Simp_tac 1);
    1.28  qed "dvd_1_left";
    1.29  AddIffs [dvd_1_left];
    1.30  
    1.31 -Goal "(m dvd 1) = (m = 1)";
    1.32 +Goal "(m dvd 1') = (m = 1')";
    1.33  by (simp_tac (simpset() addsimps [dvd_def]) 1); 
    1.34  qed "dvd_1_iff_1";
    1.35  Addsimps [dvd_1_iff_1];