src/HOL/Presburger.thy
changeset 58787 af9eb5e566dd
parent 58777 6ba2f1fa243b
child 58820 3ad2759acc52
     1.1 --- a/src/HOL/Presburger.thy	Sat Oct 25 19:20:28 2014 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Sun Oct 26 19:11:16 2014 +0100
     1.3 @@ -457,8 +457,6 @@
     1.4  context linordered_idom
     1.5  begin
     1.6  
     1.7 -declare zero_le_power_iff [presburger]
     1.8 -
     1.9  declare zero_le_power_eq [presburger]
    1.10  
    1.11  declare zero_less_power_eq [presburger]