src/HOL/Integ/IntDiv.ML
changeset 9108 9fff97d29837
parent 9063 0d7628966069
child 9367 df7a4824111e
     1.1 --- a/src/HOL/Integ/IntDiv.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntDiv.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  by (Asm_simp_tac 1);
     1.5  qed "posDivAlg_eqn";
     1.6  
     1.7 -val posDivAlg_induct = lemma RS posDivAlg.induct;
     1.8 +bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct);
     1.9  
    1.10  
    1.11  (*Correctness of posDivAlg: it computes quotients correctly*)
    1.12 @@ -146,7 +146,7 @@
    1.13  by (Asm_simp_tac 1);
    1.14  qed "negDivAlg_eqn";
    1.15  
    1.16 -val negDivAlg_induct = lemma RS negDivAlg.induct;
    1.17 +bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct);
    1.18  
    1.19  
    1.20  (*Correctness of negDivAlg: it computes quotients correctly