added code generation syntax for some char combinators
authorhaftmann
Mon Dec 18 08:21:27 2006 +0100 (2006-12-18)
changeset 218719ce66839d9f1
parent 21870 c701cdacf69b
child 21872 75ba582dd6e9
added code generation syntax for some char combinators
src/HOL/Library/Char_ord.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Char_ord.thy	Mon Dec 18 08:21:26 2006 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Mon Dec 18 08:21:27 2006 +0100
     1.3 @@ -96,4 +96,8 @@
     1.4  instance char :: linorder
     1.5    by default (auto simp: char_le_def)
     1.6  
     1.7 +code_const char_to_int_pair
     1.8 +  (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
     1.9 +  (Haskell "error/ \"char'_to'_int'_pair\"")
    1.10 +
    1.11  end
     2.1 --- a/src/HOL/List.thy	Mon Dec 18 08:21:26 2006 +0100
     2.2 +++ b/src/HOL/List.thy	Mon Dec 18 08:21:27 2006 +0100
     2.3 @@ -2555,9 +2555,12 @@
     2.4    (SML "char")
     2.5    (Haskell "Char")
     2.6  
     2.7 -code_const Char and char_rec and "size \<Colon> char \<Rightarrow> nat"
     2.8 -  (SML "raise/ Fail/ \"Char\"" and "raise/ Fail/ \"char_rec\"" and "raise/ Fail/ \"size_char\"")
     2.9 -  (Haskell "error/ \"Char\"" and "error/ \"char_rec\"" and "error/ \"size_char\"")
    2.10 +code_const Char and char_rec
    2.11 +    and char_case and "size \<Colon> char \<Rightarrow> nat"
    2.12 +  (SML "raise/ Fail/ \"Char\""
    2.13 +    and "raise/ Fail/ \"char_rec\"" and "raise/ Fail/ \"char_case\"" and "raise/ Fail/ \"size_char\"")
    2.14 +  (Haskell "error/ \"Char\""
    2.15 +    and "error/ \"char_rec\"" and "error/ \"char_case\"" and "error/ \"size_char\"")
    2.16  
    2.17  code_instance list :: eq and char :: eq
    2.18    (Haskell - and -)
    2.19 @@ -2566,6 +2569,7 @@
    2.20    (Haskell infixl 4 "==")
    2.21  
    2.22  code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    2.23 +  (SML "!((_ : char) = _)")
    2.24    (Haskell infixl 4 "==")
    2.25  
    2.26  code_reserved SML