# HG changeset patch
# User huffman
# Date 1274571946 25200
# Node ID b2073920448f444e9e14297da6439dc87f9c65a7
# Parent  665a3dfe863276320c306966bb4bf8e783ce32df
disambiguate some syntax

diff -r 665a3dfe8632 -r b2073920448f src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Sat May 22 14:04:05 2010 -0700
+++ b/src/HOL/IMP/Natural.thy	Sat May 22 16:45:46 2010 -0700
@@ -25,6 +25,16 @@
 notation (xsymbols)
   update  ("_/[_ \<mapsto> /_]" [900,0,0] 900)
 
+text {* Disable conflicting syntax from HOL Map theory. *}
+
+no_syntax
+  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
+  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
+  ""         :: "maplet => maplets"             ("_")
+  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
+  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
+  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
+
 text {*
   The big-step execution relation @{text evalc} is defined inductively:
 *}
@@ -111,7 +121,7 @@
   in the same @{text s'}}. Formally:
 *}
 definition
-  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _") where
+  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where
   "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
 
 text {*
diff -r 665a3dfe8632 -r b2073920448f src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Sat May 22 14:04:05 2010 -0700
+++ b/src/HOLCF/IMP/Denotational.thy	Sat May 22 16:45:46 2010 -0700
@@ -7,6 +7,16 @@
 
 theory Denotational imports HOLCF "../../HOL/IMP/Natural" begin
 
+text {* Disable conflicting syntax from HOL Map theory. *}
+
+no_syntax
+  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
+  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
+  ""         :: "maplet => maplets"             ("_")
+  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
+  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
+  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
+
 subsection "Definition"
 
 definition