# HG changeset patch
# User haftmann
# Date 1166426487 -3600
# Node ID 9ce66839d9f1784f1c550fdd740592a33742a3da
# Parent  c701cdacf69b9523534c4ddad33bf8eb0d05d238
added code generation syntax for some char combinators

diff -r c701cdacf69b -r 9ce66839d9f1 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Mon Dec 18 08:21:26 2006 +0100
+++ b/src/HOL/Library/Char_ord.thy	Mon Dec 18 08:21:27 2006 +0100
@@ -96,4 +96,8 @@
 instance char :: linorder
   by default (auto simp: char_le_def)
 
+code_const char_to_int_pair
+  (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
+  (Haskell "error/ \"char'_to'_int'_pair\"")
+
 end
diff -r c701cdacf69b -r 9ce66839d9f1 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 18 08:21:26 2006 +0100
+++ b/src/HOL/List.thy	Mon Dec 18 08:21:27 2006 +0100
@@ -2555,9 +2555,12 @@
   (SML "char")
   (Haskell "Char")
 
-code_const Char and char_rec and "size \<Colon> char \<Rightarrow> nat"
-  (SML "raise/ Fail/ \"Char\"" and "raise/ Fail/ \"char_rec\"" and "raise/ Fail/ \"size_char\"")
-  (Haskell "error/ \"Char\"" and "error/ \"char_rec\"" and "error/ \"size_char\"")
+code_const Char and char_rec
+    and char_case and "size \<Colon> char \<Rightarrow> nat"
+  (SML "raise/ Fail/ \"Char\""
+    and "raise/ Fail/ \"char_rec\"" and "raise/ Fail/ \"char_case\"" and "raise/ Fail/ \"size_char\"")
+  (Haskell "error/ \"Char\""
+    and "error/ \"char_rec\"" and "error/ \"char_case\"" and "error/ \"size_char\"")
 
 code_instance list :: eq and char :: eq
   (Haskell - and -)
@@ -2566,6 +2569,7 @@
   (Haskell infixl 4 "==")
 
 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) = _)")
   (Haskell infixl 4 "==")
 
 code_reserved SML