--- a/src/HOL/Library/Quotient_Option.thy Fri Apr 20 18:29:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Fri Apr 20 22:49:40 2012 +0200
@@ -78,7 +78,7 @@
"bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
unfolding bi_unique_def split_option_all by simp
-subsection {* Correspondence rules for transfer package *}
+subsection {* Transfer rules for transfer package *}
lemma None_transfer [transfer_rule]: "(option_rel A) None None"
by simp
@@ -92,7 +92,7 @@
lemma option_map_transfer [transfer_rule]:
"((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
- unfolding Option.map_def by correspondence
+ unfolding Option.map_def by transfer_prover
lemma option_bind_transfer [transfer_rule]:
"(option_rel A ===> (A ===> option_rel B) ===> option_rel B)