src/HOL/Library/Char_ord.thy
changeset 21871 9ce66839d9f1
parent 21404 eb85850d3eb7
child 21911 e29bcab0c81c
equal deleted inserted replaced
21870:c701cdacf69b 21871:9ce66839d9f1
    94   by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le)
    94   by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le)
    95 
    95 
    96 instance char :: linorder
    96 instance char :: linorder
    97   by default (auto simp: char_le_def)
    97   by default (auto simp: char_le_def)
    98 
    98 
       
    99 code_const char_to_int_pair
       
   100   (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
       
   101   (Haskell "error/ \"char'_to'_int'_pair\"")
       
   102 
    99 end
   103 end