diff -r ef1a47a4996b -r 14b2c22a7e40 src/HOL/Integ/Bin.thy --- 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*}