src/HOL/MicroJava/JVM/JVMState.thy
changeset 10042 7164dc0d24d8
parent 8034 6fc37b5c5e98
child 10057 8c8d2d0d3ef8
     1.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -32,8 +32,8 @@
     1.4  (** exceptions **)
     1.5  
     1.6  constdefs
     1.7 - raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
     1.8 -"raise_xcpt c x \\<equiv> (if c then Some x else None)"
     1.9 + raise_xcpt :: "bool => xcpt => xcpt option"
    1.10 +"raise_xcpt c x == (if c then Some x else None)"
    1.11  
    1.12  (** runtime state **)
    1.13  
    1.14 @@ -45,6 +45,6 @@
    1.15  (** dynamic method lookup **)
    1.16  
    1.17  constdefs
    1.18 - dyn_class	:: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
    1.19 -"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
    1.20 + dyn_class	:: "'code prog \\<times> sig \\<times> cname => cname"
    1.21 +"dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
    1.22  end