--- a/src/HOL/Import/HOL4Compat.thy	Mon Sep 05 17:45:37 2011 -0700
+++ b/src/HOL/Import/HOL4Compat.thy	Tue Sep 06 16:45:31 2011 +0900
@@ -63,6 +63,14 @@
 lemma OUTR: "OUTR (Inr x) = x"
   by simp
 
+lemma sum_axiom: "EX! h. h o Inl = f & h o Inr = g"
+  apply (intro allI ex1I[of _ "sum_case f g"] conjI)
+  apply (simp_all add: o_def fun_eq_iff)
+  apply (rule)
+  apply (induct_tac x)
+  apply simp_all
+  done
+
 lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
   by simp
 
@@ -491,4 +499,6 @@
 lemma real_ge: "ALL x y. (y <= x) = (y <= x)"
   by simp
 
+definition [hol4rew]: "list_mem x xs = List.member xs x"
+
 end