Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Char_ord.thy
changeset 21404 eb85850d3eb7
parent 19736 d8d0f8f51d69
child 21871 9ce66839d9f1 
--- a/src/HOL/Library/Char_ord.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/Char_ord.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -32,8 +32,8 @@
   "nibble_to_int NibbleF = 15"
 
 definition
-  int_to_nibble :: "int \<Rightarrow> nibble"
-  "int_to_nibble x \<equiv> (let y = x mod 16 in
+  int_to_nibble :: "int \<Rightarrow> nibble" where
+  "int_to_nibble x = (let y = x mod 16 in
     if y = 0 then Nibble0 else
     if y = 1 then Nibble1 else
     if y = 2 then Nibble2 else
isabelle