theory Test
imports
  Main
  "~~/src/HOL/Library/Monad_Syntax"
begin

definition double :: "nat option \<Rightarrow> nat option" where
  "double m \<equiv> do {
    x \<leftarrow> m;
    let d = x*2;
    Some d
  }"

thm double_def
thm (do_notation) double_def
text {*@{thm [display,margin=40,mode=do_notation] double_def}*}
end