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*}