--- a/src/HOL/List.thy Tue Jul 19 09:55:03 2016 +0200
+++ b/src/HOL/List.thy Tue Jul 19 14:09:55 2016 +0200
@@ -6920,6 +6920,10 @@
"((A ===> op =) ===> list_all2 A ===> rel_option A) List.find List.find"
unfolding List.find_def by transfer_prover
+lemma those_transfer [transfer_rule]:
+ "(list_all2 (rel_option P) ===> rel_option (list_all2 P)) those those"
+ unfolding List.those_def by transfer_prover
+
lemma remove1_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "(A ===> list_all2 A ===> list_all2 A) remove1 remove1"