src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 61180 e4716b792713
parent 61140 78ece168f5b5
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Sep 15 17:09:13 2015 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Sep 15 22:25:06 2015 +0200
     1.3 @@ -224,6 +224,18 @@
     1.4  code_pred List.member
     1.5    by(auto simp add: List.member_def elim: list.set_cases)
     1.6  
     1.7 +code_identifier constant member_i_i
     1.8 +   \<rightharpoonup> (SML) "List.member_i_i"
     1.9 +  and (OCaml) "List.member_i_i"
    1.10 +  and (Haskell) "List.member_i_i"
    1.11 +  and (Scala) "List.member_i_i"
    1.12 +
    1.13 +code_identifier constant member_i_o
    1.14 +   \<rightharpoonup> (SML) "List.member_i_o"
    1.15 +  and (OCaml) "List.member_i_o"
    1.16 +  and (Haskell) "List.member_i_o"
    1.17 +  and (Scala) "List.member_i_o"
    1.18 +
    1.19  section \<open>Setup for String.literal\<close>
    1.20  
    1.21  setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close>