src/HOL/List.thy
changeset 21126 4dbc3ccbaab0
parent 21113 5b76e541cc0a
child 21131 a447addc14af
equal deleted inserted replaced
21125:9b7d35ca1eef 21126:4dbc3ccbaab0
  2660 code_type char
  2660 code_type char
  2661   (SML "char")
  2661   (SML "char")
  2662   (Haskell "Char")
  2662   (Haskell "Char")
  2663 
  2663 
  2664 code_const Char
  2664 code_const Char
  2665   (SML "!(__,/ __)")
  2665   (SML "!((_),/ (_))")
  2666   (Haskell "!(__,/ __)")
  2666   (Haskell "!((_),/ (_))")
  2667 
  2667 
  2668 code_instance list :: eq and char :: eq
  2668 code_instance list :: eq and char :: eq
  2669   (Haskell - and -)
  2669   (Haskell - and -)
  2670 
  2670 
  2671 code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
  2671 code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"