src/HOL/Product_Type.thy

   by (simp add: expand_fun_eq)
 
 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
 declare prod_caseE' [elim!] prod_caseE [elim!]
 
-lemma prod_case_split [code post]:
+lemma prod_case_split:
   "prod_case = split"
   by (auto simp add: expand_fun_eq)
-
-lemmas [code inline] = prod_case_split [symmetric]
 
 
 subsection {* Further cases/induct rules for tuples *}
 
 lemma prod_cases3 [cases type]:

 
 instance * :: (eq, eq) eq ..
 
 lemma [code func]:
   "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
+
+lemma split_case_cert:
+  assumes "CASE \<equiv> split f"
+  shows "CASE (a, b) \<equiv> f a b"
+  using assms by simp
+
+setup {*
+  Code.add_case @{thm split_case_cert}
+*}
 
 code_type *
   (SML infix 2 "*")
   (OCaml infix 2 "*")
   (Haskell "!((_),/ (_))")