# HG changeset patch
# User huffman
# Date 1329816657 -3600
# Node ID 69a273fcd53a493dd70ffc29e9c173243d15c5c1
# Parent  fdb84c40e0744d63edf07ba27ee0fee9897494f8
avoid using constant Int.neg

diff -r fdb84c40e074 -r 69a273fcd53a src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Feb 21 09:17:53 2012 +0100
+++ b/src/HOL/Algebra/Group.thy	Tue Feb 21 10:30:57 2012 +0100
@@ -41,7 +41,7 @@
 begin
   definition "int_pow G a z =
    (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
-    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
+    in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
 end
 
 locale monoid =
@@ -391,7 +391,7 @@
 text {* Power *}
 
 lemma (in group) int_pow_def2:
-  "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
+  "a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"
   by (simp add: int_pow_def nat_pow_def Let_def)
 
 lemma (in group) int_pow_0 [simp]: