author | paulson |
Fri, 15 Sep 2000 12:39:57 +0200 | |
changeset 9969 | 4753185f1dd2 |
parent 8038 | a13c3b80d3d4 |
child 10042 | 7164dc0d24d8 |
permissions | -rw-r--r-- |
(* Title: HOL/MicroJava/JVM/Store.thy ID: $Id$ Author: Cornelia Pusch Copyright 1999 Technische Universitaet Muenchen The store. The JVM builds on many notions already defined in Java. Conform provides notions for the type safety proof of the Bytecode Verifier. *) Store = Conform + constdefs newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a" "newref s \\<equiv> \\<epsilon>v. s v = None" end