src/HOL/IMP/Natural.thy

   in state @{text s}, terminates in state @{text s'}}. Formally,
   @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
   @{text "(c,s,s')"} is part of the relation @{text evalc}}:
 *}
 
-constdefs
-  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
-  "update == fun_upd"
-
-syntax (xsymbols)
-  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
+definition
+  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
+  "update = fun_upd"
+
+notation (xsymbols)
+  update  ("_/[_ \<mapsto> /_]" [900,0,0] 900)
 
 text {*
   The big-step execution relation @{text evalc} is defined inductively:
 *}
 inductive

   We call two statements @{text c} and @{text c'} equivalent wrt.~the
   big-step semantics when \emph{@{text c} started in @{text s} terminates
   in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   in the same @{text s'}}. Formally:
 *}
-constdefs
-  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
-  "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
+definition
+  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _") where
+  "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
 
 text {*
   Proof rules telling Isabelle to unfold the definition
   if there is something to be proved about equivalent
   statements: *}