1.1 --- a/src/HOL/IMP/Natural.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/Natural.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -18,12 +18,12 @@
     1.4    @{text "(c,s,s')"} is part of the relation @{text evalc}}:
     1.5  *}
     1.6  
     1.7 -constdefs
     1.8 -  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
     1.9 -  "update == fun_upd"
    1.10 +definition
    1.11 +  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
    1.12 +  "update = fun_upd"
    1.13  
    1.14 -syntax (xsymbols)
    1.15 -  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
    1.16 +notation (xsymbols)
    1.17 +  update  ("_/[_ \<mapsto> /_]" [900,0,0] 900)
    1.18  
    1.19  text {*
    1.20    The big-step execution relation @{text evalc} is defined inductively:
    1.21 @@ -104,9 +104,9 @@
    1.22    in @{text s'} iff @{text c'} started in the same @{text s} also terminates
    1.23    in the same @{text s'}}. Formally:
    1.24  *}
    1.25 -constdefs
    1.26 -  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
    1.27 -  "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
    1.28 +definition
    1.29 +  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _") where
    1.30 +  "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
    1.31  
    1.32  text {*
    1.33    Proof rules telling Isabelle to unfold the definition