--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Fri Apr 02 13:33:48 2010 +0200
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Apr 07 19:17:10 2010 +0200
@@ -1,10 +1,9 @@
(* Title: HOL/Hoare/HeapSyntax.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
*)
-theory HeapSyntaxAbort imports HoareAbort Heap begin
+theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin
subsection "Field access and update"
@@ -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]