src/HOL/Integ/IntDef.ML
changeset 9108 9fff97d29837
parent 8949 d46adac29b71
child 9366 a83f3abbfc93
     1.1 --- a/src/HOL/Integ/IntDef.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4                         addSEs [sym, integ_trans_lemma]) 1);
     1.5  qed "equiv_intrel";
     1.6  
     1.7 -val equiv_intrel_iff = [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff;
     1.8 +bind_thm ("equiv_intrel_iff", [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
     1.9  
    1.10  Goalw  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
    1.11  by (Fast_tac 1);
    1.12 @@ -586,11 +586,11 @@
    1.13  (*This list of rewrites simplifies (in)equalities by bringing subtractions
    1.14    to the top and then moving negative terms to the other side.  
    1.15    Use with zadd_ac*)
    1.16 -val zcompare_rls = 
    1.17 +bind_thms ("zcompare_rls",
    1.18      [symmetric zdiff_def,
    1.19       zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
    1.20       zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, 
    1.21 -     zdiff_eq_eq, eq_zdiff_eq];
    1.22 +     zdiff_eq_eq, eq_zdiff_eq]);
    1.23  
    1.24  
    1.25  (** Cancellation laws **)