src/HOL/Bali/WellType.thy
changeset 27208 5fe899199f85
parent 24783 5a3e336a2e37
child 27239 f2f42f9fa09d
     1.1 --- a/src/HOL/Bali/WellType.thy	Sat Jun 14 17:49:24 2008 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Sat Jun 14 23:19:51 2008 +0200
     1.3 @@ -652,9 +652,13 @@
     1.4  apply (simp_all (no_asm_use) split del: split_if_asm)
     1.5  apply (safe del: disjE)
     1.6  (* 17 subgoals *)
     1.7 -apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
     1.8 +apply (tactic {* ALLGOALS (fn i =>
     1.9 +  if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
    1.10 +    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
    1.11 +    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
    1.12 +  else RuleInsts.thin_tac @{context} "All ?P" i) *})
    1.13  (*apply (safe del: disjE elim!: wt_elim_cases)*)
    1.14 -apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
    1.15 +apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
    1.16  apply (simp_all (no_asm_use) split del: split_if_asm)
    1.17  apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
    1.18  apply ((blast del: equalityCE dest: sym [THEN trans])+)