equal
deleted
inserted
replaced
1 (* Title: HOL/Integ/Bin.thy |
1 (* Title: HOL/Integ/Bin.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 David Spelt, University of Twente |
|
5 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
6 Copyright 1996 University of Twente |
5 |
|
6 Ported from ZF to HOL by David Spelt. |
7 *) |
7 *) |
8 |
8 |
9 header{*Arithmetic on Binary Integers*} |
9 header{*Arithmetic on Binary Integers*} |
10 |
10 |
11 theory Bin = IntDef + Numeral: |
11 theory Bin = IntDef + Numeral: |