# HG changeset patch
# User streckem
# Date 1001936185 -7200
# Node ID 3dfde687f0d7161a82362d1b85a7712fad55cd9f
# Parent  0b3a02daf7fb1a74b42f50ec445583b466f0e665
Removed some unfoldings of defs after declaring wf_java_prog as syntax

diff -r 0b3a02daf7fb -r 3dfde687f0d7 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Oct 01 13:33:49 2001 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Oct 01 13:36:25 2001 +0200
@@ -118,7 +118,6 @@
           xi\<le>|h' \<and> (h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));  
   G,xh\<turnstile>a'::\<preceq> Class C |] ==>  
   xc\<le>|h' \<and> (h', l)::\<preceq>(G, lT) \<and>  (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
-apply (unfold wf_java_prog_def)
 apply( drule max_spec2mheads)
 apply( clarify)
 apply( drule (2) non_np_objD')
@@ -187,7 +186,6 @@
 apply( tactic "ALLGOALS strip_tac")
 apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *})
 apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
-apply( unfold wf_java_prog_def)
 
 (* Level 7 *)
 
@@ -308,10 +306,10 @@
 apply(clarsimp)
 apply(unfold is_class_def)
 apply(clarsimp)
-apply(rule Call_type_sound [unfolded wf_java_prog_def]);
+apply(rule Call_type_sound);
 prefer 11
 apply blast
-apply (simp (no_asm_simp))+
+apply (simp (no_asm_simp))+ 
 done
 ML{*
 Unify.search_bound := 20;
@@ -342,7 +340,6 @@
   method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
 apply( drule (4) eval_type_sound)
 apply(clarsimp)
-apply(unfold wf_java_prog_def)
 apply( frule widen_methd)
 apply(   assumption)
 prefer 2