--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Feb 10 19:37:34 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Feb 10 23:53:46 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/HeapSyntax.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
*)
@@ -17,16 +16,16 @@
reason about storage allocation/deallocation. *}
syntax
- "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
("_/'((_ \<rightarrow> _)')" [1000,0] 900)
- "@fassign" :: "'a ref => id => 'v => 's com"
+ "_fassign" :: "'a ref => id => 'v => 's com"
("(2_^._ :=/ _)" [70,1000,65] 61)
- "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
+ "_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "refupdate f r v" == "f(addr r := v)"
- "p^.f := e" => "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)"
- "p^.f" => "f(addr p)"
+ "_refupdate f r v" == "f(CONST addr r := v)"
+ "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
+ "p^.f" => "f(CONST addr p)"
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]