--- a/src/HOL/Library/EfficientNat.thy Wed Feb 14 10:06:15 2007 +0100
+++ b/src/HOL/Library/EfficientNat.thy Wed Feb 14 10:06:16 2007 +0100
@@ -22,6 +22,9 @@
text {*
A int-to-nat conversion with domain
restricted to non-negative ints (in contrast to @{const nat}).
+ Note that this restriction has no logical relevance and
+ is just a kind of proof hint -- nothing prevents you from
+ writing nonsense like @{term "nat_of_int (-4)"}
*}
definition
@@ -118,7 +121,6 @@
then show ?thesis unfolding int_aux_def by simp
qed
-
subsection {* Code generator setup for basic functions *}
text {*
@@ -185,6 +187,8 @@
(OCaml "_")
(Haskell "_")
+hide const nat_of_int
+
subsection {* Preprocessors *}