# HG changeset patch
# User paulson
# Date 1196262961 -3600
# Node ID 5760991891dd062df7af63ac663744df33a3ad31
# Parent  e8ab1c42c14f043974c5e591c6e3ed3a2a345d86
comment

diff -r e8ab1c42c14f -r 5760991891dd src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Wed Nov 28 15:26:39 2007 +0100
+++ b/src/HOL/Numeral.thy	Wed Nov 28 16:16:01 2007 +0100
@@ -25,6 +25,11 @@
   even if m is negative;
   For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
   @{text "-5 = (-3)*2 + 1"}.
+  
+  This two's complement binary representation derives from the paper 
+  "An Efficient Representation of Arithmetic for Term Rewriting" by
+  Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
+  Springer LNCS 488 (240-251), 1991.
 *}
 
 datatype bit = B0 | B1