equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 2002 TUM |
4 Copyright 2002 TUM |
5 *) |
5 *) |
6 |
6 |
7 theory HeapSyntax = Hoare + Heap: |
7 theory HeapSyntax imports Hoare Heap begin |
8 |
8 |
9 subsection "Field access and update" |
9 subsection "Field access and update" |
10 |
10 |
11 syntax |
11 syntax |
12 "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
12 "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" |