equal
deleted
inserted
replaced
8 the address type. This avoids the Ref constructor and thus simplifies |
8 the address type. This avoids the Ref constructor and thus simplifies |
9 specifications (a bit). However, the proofs don't seem to get simpler |
9 specifications (a bit). However, the proofs don't seem to get simpler |
10 - in fact in some case they appear to get (a bit) more complicated. |
10 - in fact in some case they appear to get (a bit) more complicated. |
11 *) |
11 *) |
12 |
12 |
13 theory Pointers0 = Hoare: |
13 theory Pointers0 imports Hoare begin |
14 |
14 |
15 subsection "References" |
15 subsection "References" |
16 |
16 |
17 axclass ref < type |
17 axclass ref < type |
18 consts Null :: "'a::ref" |
18 consts Null :: "'a::ref" |