src/HOL/Code_Numeral.thy
changeset 60562 24af00b010cf
parent 60352 d46de31a50c4
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Jun 22 23:19:48 2015 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jun 23 16:55:28 2015 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4  
     1.5  instance integer :: semiring_numeral_div
     1.6    by intro_classes (transfer,
     1.7 -    fact semiring_numeral_div_class.le_add_diff_inverse2
     1.8 +    fact le_add_diff_inverse2
     1.9      semiring_numeral_div_class.div_less
    1.10      semiring_numeral_div_class.mod_less
    1.11      semiring_numeral_div_class.div_positive