--- a/src/Doc/Datatypes/Datatypes.thy Tue Jan 07 12:37:12 2020 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jan 07 14:58:01 2020 +0100
@@ -3022,12 +3022,7 @@
lift_bnf 'a myoption (*<*)[wits: "Inl undefined :: 'a + 'a"](*>*)
- proof (intro rel_funI)
- fix f g :: "'a \<Rightarrow> 'b" and x y :: "'a + 'a"
- assume "f = g" "ignore_Inl x y"
- then show "ignore_Inl (map_sum f f x) (map_sum g g y)"
- by (cases x; cases y) auto
- next
+ proof -
fix P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
assume "P OO Q \<noteq> bot"
then show "rel_sum P P OO ignore_Inl OO rel_sum Q Q