src/HOL/MicroJava/J/JTypeSafe.thy
changeset 22271 51a80e238b29
parent 16417 9bc16273c2d4
child 23757 087b0a241557
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Feb 07 17:41:11 2007 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Feb 07 17:44:07 2007 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  apply (case_tac "ref_ty")
     1.5  apply (clarsimp simp add: conf_def)
     1.6  apply simp
     1.7 -apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D", simp) 
     1.8 +apply (ind_cases2 "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
     1.9  apply (rule conf_widen, assumption+) apply (erule widen.subcls)
    1.10  
    1.11  apply (unfold cast_ok_def)
    1.12 @@ -205,7 +205,7 @@
    1.13  -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
    1.14  apply( simp_all)
    1.15  apply( tactic "ALLGOALS strip_tac")
    1.16 -apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
    1.17 +apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
    1.18                   THEN_ALL_NEW Full_simp_tac) *})
    1.19  apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
    1.20  
    1.21 @@ -222,7 +222,7 @@
    1.22  apply( rule conjI)
    1.23  apply(  force elim!: NewC_conforms)
    1.24  apply( rule conf_obj_AddrI)
    1.25 -apply(  rule_tac [2] rtrancl_refl)
    1.26 +apply(  rule_tac [2] rtrancl.rtrancl_refl)
    1.27  apply( simp (no_asm))
    1.28  
    1.29  -- "for Cast"
    1.30 @@ -245,22 +245,22 @@
    1.31  apply( fast elim: conforms_localD [THEN lconfD])
    1.32  
    1.33  -- "for FAss"
    1.34 -apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
    1.35 +apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
    1.36         THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
    1.37  
    1.38  -- "for if"
    1.39 -apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
    1.40 +apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 7*})
    1.41  
    1.42  apply (tactic "forward_hyp_tac")
    1.43  
    1.44  -- "11+1 if"
    1.45 -prefer 8
    1.46 +prefer 7
    1.47  apply(  fast intro: hext_trans)
    1.48 -prefer 8
    1.49 +prefer 7
    1.50  apply(  fast intro: hext_trans)
    1.51  
    1.52  -- "10 Expr"
    1.53 -prefer 7
    1.54 +prefer 6
    1.55  apply( fast)
    1.56  
    1.57  -- "9 ???"
    1.58 @@ -280,7 +280,7 @@
    1.59  
    1.60  -- "7 LAss"
    1.61  apply (fold fun_upd_def)
    1.62 -apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
    1.63 +apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
    1.64                   THEN_ALL_NEW Full_simp_tac) 1 *})
    1.65  apply (intro strip)
    1.66  apply (case_tac E)
    1.67 @@ -315,7 +315,7 @@
    1.68  
    1.69  
    1.70  -- "2 FAss"
    1.71 -apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)")
    1.72 +apply (subgoal_tac "(np a' x1, aa, ba) ::\<preceq> (G, lT)")
    1.73    prefer 2
    1.74    apply (simp add: np_def)
    1.75    apply (fast intro: conforms_xcpt_change xconf_raise_if)