| changeset 10058 | 7b2be4d2703a |
| parent 10057 | 8c8d2d0d3ef8 |
| child 10059 | f56da4769355 |
| 10057:8c8d2d0d3ef8 | 10058:7b2be4d2703a |
|---|---|
1 (* Title: HOL/MicroJava/JVM/Store.thy |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 Goalw [newref_def] |
|
8 "hp x = None --> hp (newref hp) = None"; |
|
9 by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1); |
|
10 qed_spec_mp "newref_None"; |