# HG changeset patch
# User wenzelm
# Date 1451737774 -3600
# Node ID b3cda398a5b1f45d1b08beb412d0015d527908ca
# Parent  91fcb3bc28bb6fb2382539e4518af280de340d80
more symbols;

diff -r 91fcb3bc28bb -r b3cda398a5b1 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Sat Jan 02 13:22:46 2016 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Sat Jan 02 13:29:34 2016 +0100
@@ -48,17 +48,17 @@
 
 translations
   "_do_block (_do_cons (_do_then t) (_do_final e))"
-    == "CONST bind_do t (\<lambda>_. e)"
+    \<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
   "_do_block (_do_cons (_do_bind p t) (_do_final e))"
-    == "CONST bind_do t (\<lambda>p. e)"
+    \<rightleftharpoons> "CONST bind_do t (\<lambda>p. e)"
   "_do_block (_do_cons (_do_let p t) bs)"
-    == "let p = t in _do_block bs"
+    \<rightleftharpoons> "let p = t in _do_block bs"
   "_do_block (_do_cons b (_do_cons c cs))"
-    == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
+    \<rightleftharpoons> "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
   "_do_cons (_do_let p t) (_do_final s)"
-    == "_do_final (let p = t in s)"
+    \<rightleftharpoons> "_do_final (let p = t in s)"
   "_do_block (_do_final e)" => "e"
-  "(m \<then> n)" => "(m \<bind> (\<lambda>_. n))"
+  "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
 
 adhoc_overloading
   bind Set.bind Predicate.bind Option.bind List.bind