--- 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 {*
--- 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