| changeset 29629 | 5111ce425e7a |
| parent 29025 | 8c8859c0d734 |
| child 29997 | f6756c097c2d |
| child 30240 | 5b25fee0362c |
--- a/src/HOL/Library/Numeral_Type.thy Mon Jan 26 22:14:16 2009 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Mon Jan 26 22:14:17 2009 +0100 @@ -1,11 +1,8 @@ -(* - ID: $Id$ - Author: Brian Huffman - - Numeral Syntax for Types +(* Title: HOL/Library/Numeral_Type.thy + Author: Brian Huffman *) -header "Numeral Syntax for Types" +header {* Numeral Syntax for Types *} theory Numeral_Type imports Plain "~~/src/HOL/Presburger"