1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 06 10:48:16 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 06 11:00:57 2010 +0200
     1.3 @@ -82,9 +82,6 @@
     1.4    raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
     1.5    [code del]: "raise s = Heap (Pair (Inr Exn))"
     1.6  
     1.7 -notation (latex output)
     1.8 -  "raise" ("\<^raw:{\textsf{raise}}>")
     1.9 -
    1.10  lemma execute_raise [simp]:
    1.11    "execute (raise s) h = (Inr Exn, h)"
    1.12    by (simp add: raise_def)
    1.13 @@ -115,13 +112,6 @@
    1.14  syntax (xsymbols)
    1.15    "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.16      ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
    1.17 -syntax (latex output)
    1.18 -  "_do" :: "do_expr \<Rightarrow> 'a"
    1.19 -    ("(\<^raw:{\textsf{do}}> (_))" [12] 100)
    1.20 -  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.21 -    ("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12)
    1.22 -notation (latex output)
    1.23 -  "return" ("\<^raw:{\textsf{return}}>")
    1.24  
    1.25  translations
    1.26    "_do f" => "f"