changeset 779 | 3b21b24a5fb6 |
parent 698 | ed44eaaea63e |
child 829 | 42b90994ac77 |
--- a/Quot/QuotOption.thy Tue Dec 22 22:10:48 2009 +0100 +++ b/Quot/QuotOption.thy Wed Dec 23 10:31:54 2009 +0100 @@ -16,7 +16,8 @@ "option_map f None = None" | "option_map f (Some x) = Some (f x)" -declare [[map * = (option_map, option_rel)]] +declare [[map option = (option_map, option_rel)]] + lemma option_quotient[quot_thm]: assumes q: "Quotient R Abs Rep"