author | nipkow |
Thu, 11 Nov 1999 12:23:45 +0100 | |
changeset 8011 | d14c4e9e9c8e |
child 9969 | 4753185f1dd2 |
permissions | -rw-r--r-- |
8011 | 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 \\<longrightarrow> hp (newref hp) = None"; |
|
9 |
by (fast_tac (claset() addIs [selectI2EX] addss (simpset())) 1); |
|
10 |
qed_spec_mp "newref_None"; |