# 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\|h' \ (h', xj)::\(G, lT) \ (x' = None --> G,h'\v::\T)); G,xh\a'::\ Class C |] ==> xc\|h' \ (h', l)::\(G, lT) \ (x' = None --> G,h'\v::\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 \ None" apply( drule (4) eval_type_sound) apply(clarsimp) -apply(unfold wf_java_prog_def) apply( frule widen_methd) apply( assumption) prefer 2