--- a/src/HOL/MicroJava/JVM/JVMState.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Thu Sep 21 10:42:49 2000 +0200
@@ -32,8 +32,8 @@
(** exceptions **)
constdefs
- raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
-"raise_xcpt c x \\<equiv> (if c then Some x else None)"
+ raise_xcpt :: "bool => xcpt => xcpt option"
+"raise_xcpt c x == (if c then Some x else None)"
(** runtime state **)
@@ -45,6 +45,6 @@
(** dynamic method lookup **)
constdefs
- dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
-"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
+ dyn_class :: "'code prog \\<times> sig \\<times> cname => cname"
+"dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
end