isabelle: src/HOL/MicroJava/JVM/Store.ML@09bf8fcd1c6e (annotated)

8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/MicroJava/JVM/Store.thy
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	2	ID: $Id$
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	Author: Cornelia Pusch
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	4	Copyright 1999 Technische Universitaet Muenchen
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	5	*)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	6
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	7	Goalw [newref_def]
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	8	"hp x = None \\<longrightarrow> hp (newref hp) = None";
9998 09bf8fcd1c6e fixed someI2_ex; wenzelm parents: 9969 diff changeset	9	by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	10	qed_spec_mp "newref_None";