author | kleing |
Thu, 21 Sep 2000 10:42:49 +0200 | |
changeset 10042 | 7164dc0d24d8 |
parent 8038 | a13c3b80d3d4 |
child 10057 | 8c8d2d0d3ef8 |
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) => 'a" "newref s == SOME v. s v = None" end