--- a/src/HOLCF/Lift.thy Wed Mar 24 15:21:42 2010 +0100
+++ b/src/HOLCF/Lift.thy Wed Mar 24 07:50:21 2010 -0700
@@ -170,28 +170,6 @@
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cases x, simp_all)
-text {*
- \medskip Extension of @{text cont_tac} and installation of simplifier.
-*}
-
-lemmas cont_lemmas_ext =
- cont2cont_flift1 cont2cont_lift_case cont2cont_lambda
- cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
-
-ML {*
-local
- val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext";
- val flift1_def = thm "flift1_def";
-in
-
-fun cont_tac i = resolve_tac cont_lemmas2 i;
-fun cont_tacR i = REPEAT (cont_tac i);
-
-fun cont_tacRs ss i =
- simp_tac ss i THEN
- REPEAT (cont_tac i)
-end;
-*}
subsection {* Lifted countable types are bifinite *}
--- a/src/HOLCF/ex/Dagstuhl.thy Wed Mar 24 15:21:42 2010 +0100
+++ b/src/HOLCF/ex/Dagstuhl.thy Wed Mar 24 07:50:21 2010 -0700
@@ -72,7 +72,7 @@
apply (unfold YYS_def)
apply (rule fix_least)
apply (subst beta_cfun)
- apply (tactic "cont_tacR 1")
+ apply simp
apply (simp add: YS_def2 [symmetric])
done
--- a/src/HOLCF/ex/Hoare.thy Wed Mar 24 15:21:42 2010 +0100
+++ b/src/HOLCF/ex/Hoare.thy Wed Mar 24 07:50:21 2010 -0700
@@ -232,12 +232,8 @@
lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (rule allI)
-apply (subst Rep_CFun_strict1)
-apply (rule refl)
+apply simp
+apply simp
apply (simp (no_asm))
apply (rule allI)
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
@@ -256,12 +252,8 @@
lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (rule allI)
-apply (subst Rep_CFun_strict1)
-apply (rule refl)
+apply simp
+apply simp
apply (rule allI)
apply (simp (no_asm))
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
@@ -285,12 +277,8 @@
lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (rule allI)
-apply (subst Rep_CFun_strict1)
-apply (rule refl)
+apply simp
+apply simp
apply (rule allI)
apply (simp (no_asm))
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
--- a/src/HOLCF/ex/Loop.thy Wed Mar 24 15:21:42 2010 +0100
+++ b/src/HOLCF/ex/Loop.thy Wed Mar 24 07:50:21 2010 -0700
@@ -137,10 +137,8 @@
ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
apply (simplesubst while_def2)
apply (rule fix_ind)
-apply (rule adm_all)
-apply (rule adm_eq)
-apply (tactic "cont_tacR 1")
-apply (simp (no_asm))
+apply simp
+apply simp
apply (rule allI)
apply (simp (no_asm))
apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)