summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Efficient_Nat.thy

changeset 37388 | 793618618f78 |

parent 37223 | 5226259b6fa2 |

child 37846 | 6f8b1bb4d248 |

1.1 --- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 08 16:37:19 2010 +0200 1.2 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 08 16:37:22 2010 +0200 1.3 @@ -11,7 +11,7 @@ 1.4 text {* 1.5 When generating code for functions on natural numbers, the 1.6 canonical representation using @{term "0::nat"} and 1.7 - @{term "Suc"} is unsuitable for computations involving large 1.8 + @{term Suc} is unsuitable for computations involving large 1.9 numbers. The efficiency of the generated code can be improved 1.10 drastically by implementing natural numbers by target-language 1.11 integers. To do this, just include this theory. 1.12 @@ -362,7 +362,7 @@ 1.13 Since natural numbers are implemented 1.14 using integers in ML, the coercion function @{const "of_nat"} of type 1.15 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function. 1.16 - For the @{const "nat"} function for converting an integer to a natural 1.17 + For the @{const nat} function for converting an integer to a natural 1.18 number, we give a specific implementation using an ML function that 1.19 returns its input value, provided that it is non-negative, and otherwise 1.20 returns @{text "0"}.