--- a/src/HOL/MicroJava/JVM/JVMExec.thy Mon Mar 01 12:30:55 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Mon Mar 01 13:42:31 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/JVM/JVMExec.thy
- ID: $Id$
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -26,9 +25,8 @@
"exec (G, Some xp, hp, frs) = None"
-constdefs
- exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ |- _ -jvm-> _" [61,61,61]60)
+definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
+ ("_ |- _ -jvm-> _" [61,61,61]60) where
"G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
@@ -41,8 +39,7 @@
@{text this} pointer of the frame is set to @{text Null} to simulate
a static method invokation.
*}
-constdefs
- start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state"
+definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where
"start_state G C m \<equiv>
let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
(None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])"