| changeset 21834 | 770ce948a59b |
| parent 21820 | 2f2b6a965ccc |
| child 22187 | a2c4861363d5 |
--- a/src/HOL/Integ/Numeral.thy Wed Dec 13 20:38:17 2006 +0100 +++ b/src/HOL/Integ/Numeral.thy Wed Dec 13 20:38:18 2006 +0100 @@ -24,7 +24,7 @@ *} text{* - This datatype avoids the use of type @{typ bool}, which would make + This type avoids the use of type @{typ bool}, which would make all of the rewrite rules higher-order. *}