src/HOL/Integ/IntDef.ML
changeset 11464 ddea204de5bc
parent 10834 a7897aebbffc
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Integ/IntDef.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4  by (asm_simp_tac (simpset() addsimps [zmult]) 1);
     1.5  qed "zmult_int0";
     1.6  
     1.7 -Goalw [int_def] "int 1 * z = z";
     1.8 +Goalw [int_def] "int 1' * z = z";
     1.9  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
    1.10  by (asm_simp_tac (simpset() addsimps [zmult]) 1);
    1.11  qed "zmult_int1";
    1.12 @@ -335,7 +335,7 @@
    1.13  by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
    1.14  qed "zmult_int0_right";
    1.15  
    1.16 -Goal "z * int 1 = z";
    1.17 +Goal "z * int 1' = z";
    1.18  by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
    1.19  qed "zmult_int1_right";
    1.20