--- a/src/HOL/Library/Quotient_Option.thy Thu Apr 26 01:05:06 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Thu Apr 26 12:01:58 2012 +0200
@@ -101,15 +101,13 @@
subsection {* Setup for lifting package *}
-lemma Quotient_option:
+lemma Quotient_option[quot_map]:
assumes "Quotient R Abs Rep T"
shows "Quotient (option_rel R) (Option.map Abs)
(Option.map Rep) (option_rel T)"
using assms unfolding Quotient_alt_def option_rel_unfold
by (simp split: option.split)
-declare [[map option = (option_rel, Quotient_option)]]
-
fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
where
"option_pred R None = True"