src/HOL/Code_Numeral.thy
changeset 59816 034b13f4efae
parent 59487 adaa430fc0f7
child 60352 d46de31a50c4
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Mar 23 19:05:14 2015 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Mar 23 19:05:14 2015 +0100
     1.3 @@ -217,9 +217,7 @@
     1.4  
     1.5  instance integer :: semiring_numeral_div
     1.6    by intro_classes (transfer,
     1.7 -    fact semiring_numeral_div_class.diff_invert_add1
     1.8 -    semiring_numeral_div_class.le_add_diff_inverse2
     1.9 -    semiring_numeral_div_class.mult_div_cancel
    1.10 +    fact semiring_numeral_div_class.le_add_diff_inverse2
    1.11      semiring_numeral_div_class.div_less
    1.12      semiring_numeral_div_class.mod_less
    1.13      semiring_numeral_div_class.div_positive