src/HOL/Integ/Bin.thy
changeset 14705 14b2c22a7e40
parent 14479 0eca4aabf371
child 14738 83f1a514dcb4
--- a/src/HOL/Integ/Bin.thy	Thu May 06 12:42:20 2004 +0200
+++ b/src/HOL/Integ/Bin.thy	Thu May 06 12:43:00 2004 +0200
@@ -1,9 +1,9 @@
 (*  Title:	HOL/Integ/Bin.thy
     ID:         $Id$
     Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
-		David Spelt, University of Twente
     Copyright	1994  University of Cambridge
-    Copyright   1996 University of Twente
+
+Ported from ZF to HOL by David Spelt.
 *)
 
 header{*Arithmetic on Binary Integers*}