# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1468930195 -7200
# Node ID 32da860241b8e9acf5d7d1ba4332fa517fa824ec
# Parent  2803d2b8f85d08d0803db95193a09373f5104e7d
added missing transfer rule

diff -r 2803d2b8f85d -r 32da860241b8 src/HOL/List.thy
--- 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"