# HG changeset patch
# User berghofe
# Date 958404845 -7200
# Node ID ac86b3d4473016fe9a334ee28c1d23a4f6e53701
# Parent  3242637f668c765cfc6b5d10005df0aaffa53944
Replaced some definitions involving epsilon by more readable primrec
definitions.

diff -r 3242637f668c -r ac86b3d44730 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Mon May 15 17:32:39 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Mon May 15 17:34:05 2000 +0200
@@ -38,7 +38,7 @@
 by( strip_tac1 1);
 by( dtac non_npD 1);
 by(  atac 1);
-by( rewrite_goals_tac [the_Addr_def,obj_ty_def]);
+by( rewrite_goals_tac [obj_ty_def]);
 by Auto_tac ;
 by(  ALLGOALS (rtac conf_AddrI));
 by     Auto_tac;
diff -r 3242637f668c -r ac86b3d44730 src/HOL/MicroJava/J/State.ML
--- a/src/HOL/MicroJava/J/State.ML	Mon May 15 17:32:39 2000 +0200
+++ b/src/HOL/MicroJava/J/State.ML	Mon May 15 17:34:05 2000 +0200
@@ -4,11 +4,6 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-val the_Addr_Addr = prove_goalw thy [the_Addr_def] 
-	"the_Addr (Addr a) = a" (K [Auto_tac]);
-
-Addsimps [the_Addr_Addr];
-
 val obj_ty_def2 = prove_goalw thy [obj_ty_def] "obj_ty (C,fs) = Class C" 
 	(K [Simp_tac 1]);
 
diff -r 3242637f668c -r ac86b3d44730 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Mon May 15 17:32:39 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Mon May 15 17:34:05 2000 +0200
@@ -8,23 +8,24 @@
 
 State = WellType +
 
-constdefs
-
+consts
   the_Bool	:: "val \\<Rightarrow> bool"
- "the_Bool v  \\<equiv> \\<epsilon>b. v = Bool b"
-
   the_Int	:: "val \\<Rightarrow> int"
- "the_Int  v  \\<equiv> \\<epsilon>i. v = Intg i"
-
   the_Addr	:: "val \\<Rightarrow> loc"
- "the_Addr  v  \\<equiv> \\<epsilon>a. v = Addr a"
-
-consts
 
   defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
   default_val	:: "ty \\<Rightarrow> val"		(* default value for all types *)
 
 primrec
+ "the_Bool (Bool b) = b"
+
+primrec
+ "the_Int (Intg i) = i"
+
+primrec
+ "the_Addr (Addr a) = a"
+
+primrec
 	"defpval Void    = Unit"
 	"defpval Boolean = Bool False"
 	"defpval Integer = Intg (#0)"