src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 36078 59f6773a7d1d
parent 36057 ca6610908ae9
child 36176 3fe7e97ccca8
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 06 10:48:16 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 06 11:00:57 2010 +0200
@@ -82,9 +82,6 @@
   raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   [code del]: "raise s = Heap (Pair (Inr Exn))"
 
-notation (latex output)
-  "raise" ("\<^raw:{\textsf{raise}}>")
-
 lemma execute_raise [simp]:
   "execute (raise s) h = (Inr Exn, h)"
   by (simp add: raise_def)
@@ -115,13 +112,6 @@
 syntax (xsymbols)
   "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
     ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
-syntax (latex output)
-  "_do" :: "do_expr \<Rightarrow> 'a"
-    ("(\<^raw:{\textsf{do}}> (_))" [12] 100)
-  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
-    ("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12)
-notation (latex output)
-  "return" ("\<^raw:{\textsf{return}}>")
 
 translations
   "_do f" => "f"