--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Mon Jun 09 17:07:08 2008 +0200
@@ -1207,7 +1207,7 @@
--{* 34 subgoals left *}
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
-apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
+apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
apply(simp_all add:Graph10)
--{* 47 subgoals left *}
apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
--- a/src/HOL/HoareParallel/OG_Examples.thy Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Mon Jun 09 17:07:08 2008 +0200
@@ -196,7 +196,7 @@
apply fastsimp
--{* 5 subgoals left *}
prefer 5
-apply(tactic {* ALLGOALS (case_tac "j=k") *})
+apply(case_tac [!] "j=k")
--{* 10 subgoals left *}
apply simp_all
apply(erule_tac x=k in allE)
@@ -502,8 +502,8 @@
lemma Example2_lemma2_aux2:
"!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
-apply(induct j)
- apply (simp_all cong:setsum_cong)
+apply(induct j)
+ apply simp_all
done
lemma Example2_lemma2:
--- a/src/HOL/Nominal/nominal_atoms.ML Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon Jun 09 17:07:08 2008 +0200
@@ -94,7 +94,7 @@
val stmnt2 = HOLogic.mk_Trueprop
(HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
- val proof2 = fn _ => EVERY [case_tac "y" 1,
+ val proof2 = fn _ => EVERY [DatatypePackage.case_tac "y" 1,
asm_simp_tac (HOL_basic_ss addsimps simp1) 1,
rtac @{thm exI} 1,
rtac @{thm refl} 1]
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Sun Jun 08 14:31:06 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 09 17:07:08 2008 +0200
@@ -96,7 +96,7 @@
in pg'' thy defs t tacs end;
fun case_UU_tac rews i v =
- case_tac (v^"=UU") i THEN
+ DatatypePackage.case_tac (v^"=UU") i THEN
asm_simp_tac (HOLCF_ss addsimps rews) i;
val chain_tac =
@@ -647,7 +647,7 @@
fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
val tacs = [
- induct_tac "n" 1,
+ DatatypePackage.induct_tac "n" 1,
simp_tac iterate_Cprod_ss 1,
asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
in pg copy_take_defs goal tacs end;
@@ -678,7 +678,7 @@
fun eq_tacs ((dn, _), cons) = map con_tac cons;
val tacs =
simp_tac iterate_Cprod_ss 1 ::
- induct_tac "n" 1 ::
+ DatatypePackage.induct_tac "n" 1 ::
simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
TRY (safe_tac HOL_cs) ::
@@ -750,7 +750,7 @@
val tacs1 = [
quant_tac 1,
simp_tac HOL_ss 1,
- induct_tac "n" 1,
+ DatatypePackage.induct_tac "n" 1,
simp_tac (take_ss addsimps prems) 1,
TRY (safe_tac HOL_cs)];
fun arg_tac arg =
@@ -845,7 +845,7 @@
maps con_tacs cons;
val tacs =
rtac allI 1 ::
- induct_tac "n" 1 ::
+ DatatypePackage.induct_tac "n" 1 ::
simp_tac take_ss 1 ::
TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
flat (mapn foo_tacs 1 (conss ~~ cases));
@@ -938,7 +938,7 @@
REPEAT (CHANGED (asm_simp_tac take_ss 1))];
val tacs = [
rtac impI 1,
- induct_tac "n" 1,
+ DatatypePackage.induct_tac "n" 1,
simp_tac take_ss 1,
safe_tac HOL_cs] @
flat (mapn x_tacs 0 xs);