src/HOL/Hoare/Pointers0.thy
changeset 35101 6ce9177d6b38
parent 17778 93d7e524417a
child 35316 870dfea4f9c0
     1.1 --- a/src/HOL/Hoare/Pointers0.thy	Wed Feb 10 19:37:34 2010 +0100
     1.2 +++ b/src/HOL/Hoare/Pointers0.thy	Wed Feb 10 23:53:46 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Hoare/Pointers.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7      Copyright   2002 TUM
     1.8  
     1.9 @@ -20,12 +19,12 @@
    1.10  subsection "Field access and update"
    1.11  
    1.12  syntax
    1.13 -  "@fassign"  :: "'a::ref => id => 'v => 's com"
    1.14 +  "_fassign"  :: "'a::ref => id => 'v => 's com"
    1.15     ("(2_^._ :=/ _)" [70,1000,65] 61)
    1.16 -  "@faccess"  :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
    1.17 +  "_faccess"  :: "'a::ref => ('a::ref \<Rightarrow> 'v) => 'v"
    1.18     ("_^._" [65,1000] 65)
    1.19  translations
    1.20 -  "p^.f := e"  =>  "f := fun_upd f p e"
    1.21 +  "p^.f := e"  =>  "f := CONST fun_upd f p e"
    1.22    "p^.f"       =>  "f p"
    1.23  
    1.24