src/HOL/Presburger.thy
changeset 30027 ab40c5e007e0
parent 29707 01cae7ad8576
child 30031 bd786c37af84
     1.1 --- a/src/HOL/Presburger.thy	Fri Feb 20 16:48:17 2009 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Fri Feb 20 20:50:49 2009 +0100
     1.3 @@ -424,7 +424,7 @@
     1.4  declare zmod_self[presburger]
     1.5  declare mod_self[presburger]
     1.6  declare mod_by_0[presburger]
     1.7 -declare nat_mod_div_trivial[presburger]
     1.8 +declare mod_div_trivial[presburger]
     1.9  declare div_mod_equality2[presburger]
    1.10  declare div_mod_equality[presburger]
    1.11  declare mod_div_equality2[presburger]