src/HOL/Library/Char_ord.thy
changeset 21871 9ce66839d9f1
parent 21404 eb85850d3eb7
child 21911 e29bcab0c81c
     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