# HG changeset patch
# User haftmann
# Date 1171443976 -3600
# Node ID d5260836d66263bc186f8d1e0f68efa4dd5d4f2a
# Parent  6f162dd72f60a5586a6ff250737bc5f5262d4d69
clarified explanation

diff -r 6f162dd72f60 -r d5260836d662 src/HOL/Library/EfficientNat.thy
--- 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 *}