# HG changeset patch
# User oheimb
# Date 830271863 -7200
# Node ID 36ba4da350c34df12b21bee261542fe8ef65a20a
# Parent  33aff4d854e49e0b6b21a59e86810390f68e71d1
adapted several proofs

diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Cfun3.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -306,7 +306,7 @@
         [
         (rtac contlubI 1),
         (strip_tac 1),
-        (res_inst_tac [("Q","lub(range(Y))=(UU::'a)")] classical2 1),
+        (case_tac "lub(range(Y))=(UU::'a)" 1),
         (res_inst_tac [("t","lub(range(Y))")] subst 1),
         (rtac sym 1),
         (atac 1),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Fix.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -31,7 +31,10 @@
         [
         (nat_ind_tac "n" 1),
         (Simp_tac 1),
-        (Asm_simp_tac 1)
+	(rtac (iterate_Suc RS ssubst) 1),
+	(rtac (iterate_Suc RS ssubst) 1),
+	(etac ssubst 1),
+	(rtac refl 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
@@ -554,7 +557,7 @@
         (rewtac max_in_chain_def),
         (cut_facts_tac prems 1),
         (strip_tac 1),
-        (res_inst_tac [("Q","!i.Y(i)=UU")] classical2 1),
+        (case_tac "!i.Y(i)=UU" 1),
         (res_inst_tac [("x","0")] exI 1),
         (strip_tac 1),
         (rtac trans 1),
@@ -708,13 +711,13 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("Q","f`(x::'a)=(UU::'b)")] classical2 1),
+        (case_tac "f`(x::'a)=(UU::'b)" 1),
         (rtac disjI1 1),
         (rtac UU_I 1),
         (res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1),
         (atac 1),
         (rtac (minimal RS monofun_cfun_arg) 1),
-        (res_inst_tac [("Q","f`(UU::'a)=(UU::'b)")] classical2 1),
+        (case_tac "f`(UU::'a)=(UU::'b)" 1),
         (etac disjI1 1),
         (rtac disjI2 1),
         (rtac allI 1),
@@ -950,7 +953,8 @@
         (etac (is_chainE RS spec) 1),
         (hyp_subst_tac 1),
         (Asm_simp_tac 1),
-        (Asm_simp_tac 1)
+        (Asm_simp_tac 1),
+	(asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
         ]);
 
 qed_goal "adm_disj_lemma4"  Fix.thy
@@ -1035,7 +1039,7 @@
 
 qed_goal "adm_disj_lemma7"  Fix.thy 
 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
-\         is_chain(%m. Y(theleast(%j. m<j & P(Y(j)))))"
+\         is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1043,33 +1047,33 @@
         (rtac allI 1),
         (rtac chain_mono3 1),
         (atac 1),
-        (rtac theleast2 1),
+        (rtac Least_le 1),
         (rtac conjI 1),
         (rtac Suc_lessD 1),
         (etac allE 1),
         (etac exE 1),
-        (rtac (theleast1 RS conjunct1) 1),
+        (rtac (LeastI RS conjunct1) 1),
         (atac 1),
         (etac allE 1),
         (etac exE 1),
-        (rtac (theleast1 RS conjunct2) 1),
+        (rtac (LeastI RS conjunct2) 1),
         (atac 1)
         ]);
 
 qed_goal "adm_disj_lemma8"  Fix.thy 
-"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(theleast(%j. m<j & P(Y(j)))))"
+"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(Least(%j. m<j & P(Y(j)))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (strip_tac 1),
         (etac allE 1),
         (etac exE 1),
-        (etac (theleast1 RS conjunct2) 1)
+        (etac (LeastI RS conjunct2) 1)
         ]);
 
 qed_goal "adm_disj_lemma9"  Fix.thy
 "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
-\         lub(range(Y)) = lub(range(%m. Y(theleast(%j. m<j & P(Y(j))))))"
+\         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1084,7 +1088,7 @@
         (atac 1),
         (etac allE 1),
         (etac exE 1),
-        (rtac (theleast1 RS conjunct1) 1),
+        (rtac (LeastI RS conjunct1) 1),
         (atac 1),
         (rtac lub_mono3 1),
         (rtac adm_disj_lemma7 1),
@@ -1104,7 +1108,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("x","%m. Y(theleast(%j. m<j & P(Y(j))))")] exI 1),
+        (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1),
         (rtac conjI 1),
         (rtac adm_disj_lemma7 1),
         (atac 1),
@@ -1172,8 +1176,37 @@
         ]);
 
 
+qed_goal "adm_not_conj"  Fix.thy  
+ "Ë adm (³x. ¿ P x); adm (³x. ¿ Q x) Ì êë adm (³x. ¿ (P x À Q x))" (fn prems =>[
+	cut_facts_tac prems 1,
+	subgoal_tac 
+	"(³x. ¿ (P x À Q x)) = (³x. ¿ P x Á ¿ Q x)" 1,
+	rtac ext 2,
+	fast_tac HOL_cs 2,
+	etac ssubst 1,
+	etac adm_disj 1,
+	atac 1]);
+
+qed_goalw "admI" Fix.thy [adm_def]
+ "(ÄY. Ë is_chain Y ; Âi. P(Y i) ; Âi. Ãj. i < j À Y i Û Y j À Y i Ý Y j Ì êë \
+\ P(lub (range Y))) êë adm P" 
+ (fn prems => [
+	strip_tac 1,
+	case_tac "finite_chain Y" 1,
+	rewtac finite_chain_def,
+	safe_tac HOL_cs,
+	dtac lub_finch1 1,
+	atac 1,
+	dtac thelubI 1,
+	etac ssubst 1,
+	etac spec 1,
+	etac swap 1,
+	rewtac max_in_chain_def,
+	resolve_tac prems 1, atac 1, atac 1,
+	fast_tac (HOL_cs addDs [le_imp_less_or_eq] 
+			 addEs [chain_mono RS mp]) 1]);
 
 val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
-        adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
+        adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less
         ];
 
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Holcfb.ML
--- a/src/HOLCF/Holcfb.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Holcfb.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -1,10 +1,10 @@
 (*  Title:      HOLCF/holcfb.ML
     ID:         $Id$
     Author:     Franz Regensburger
+    Changed by: David von Oheimb
     Copyright   1993  Technische Universitaet Muenchen
+*)
 
-Lemmas for Holcfb.thy 
-*)
 
 open Holcfb;
 
@@ -12,6 +12,7 @@
 (* <::nat=>nat=>bool is a well-ordering                                     *)
 (* ------------------------------------------------------------------------ *)
 
+(*
 qed_goal "well_ordering_nat"  Nat.thy 
         "!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
  (fn prems =>
@@ -34,12 +35,13 @@
         (rtac leI  1),
         (fast_tac HOL_cs 1)
         ]);
-
+*)
 
 (* ------------------------------------------------------------------------ *)
 (* Lemmas for selecting the least element in a nonempty set                 *)
 (* ------------------------------------------------------------------------ *)
 
+(*
 qed_goalw "theleast"  Holcfb.thy [theleast_def] 
 "P(x) ==> P(theleast(P)) & (!x.P(x)--> theleast(P) <= x)"
  (fn prems =>
@@ -50,10 +52,17 @@
         (rtac selectI 1),
         (atac 1)
         ]);
+*)
 
+
+(* val theleast1 = LeastI "?P ?k êë ?P (´x. ?P x)" *)
+(*
 val theleast1= theleast RS conjunct1;
 (* ?P1(?x1) ==> ?P1(theleast(?P1)) *)
+*)
 
+(* val theleast2 = Least_le "?P ?k êë (´x. ?P x) <= ?k" *)
+(*
 qed_goal "theleast2"  Holcfb.thy  "P(x) ==> theleast(P) <= x"
  (fn prems =>
         [
@@ -61,81 +70,39 @@
         (resolve_tac prems 1),
         (resolve_tac prems 1)
         ]);
-
+*)
 
 (* ------------------------------------------------------------------------ *)
 (* Some lemmas in HOL.thy                                                   *)
 (* ------------------------------------------------------------------------ *)
 
 
-qed_goal "de_morgan1" HOL.thy "(~a & ~b)=(~(a | b))"
-(fn prems =>
-        [
-        (rtac iffI 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
+(* val de_morgan1 = de_Morgan_disj RS sym;   "(~a & ~b)=(~(a | b))" *)
 
-qed_goal "de_morgan2" HOL.thy "(~a | ~b)=(~(a & b))"
-(fn prems =>
-        [
-        (rtac iffI 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
+(* val de_morgan2 = de_Morgan_conj RS sym;   "(~a | ~b)=(~(a & b))" *)
 
 
-qed_goal "notall2ex" HOL.thy "(~ (!x.P(x))) = (? x.~P(x))"
-(fn prems =>
-        [
-        (rtac iffI 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
+(* val notall2ex = not_all 		     "(~ (!x.P(x))) = (? x.~P(x))" *)
 
-qed_goal "notex2all" HOL.thy "(~ (? x.P(x))) = (!x.~P(x))"
-(fn prems =>
-        [
-        (rtac iffI 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
+(* val notex2all = not_ex		     "(~ (? x.P(x))) = (!x.~P(x))" *)
 
 
-qed_goal "selectI3" HOL.thy "(? x. P(x)) ==> P(@ x.P(x))"
-(fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac exE 1),
-        (etac selectI 1)
-        ]);
+(* val selectI3 =  select_eq_Ex RS iffD2   "(? x. P(x)) ==> P(@ x.P(x))" *)
 
-qed_goal "selectE" HOL.thy "P(@ x.P(x)) ==> (? x. P(x))"
-(fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac exI 1)
-        ]);
-
-qed_goal "select_eq_Ex" HOL.thy "(P(@ x.P(x))) =  (? x. P(x))"
-(fn prems =>
-        [
-        (rtac (iff RS mp  RS mp) 1),
-        (strip_tac 1),
-        (etac selectE 1),
-        (strip_tac 1),
-        (etac selectI3 1)
-        ]);
+(* val selectE =   select_eq_Ex RS iffD1   "P(@ x.P(x)) ==> (? x. P(x))" *)
 
 
+(*
 qed_goal "notnotI" HOL.thy "P ==> ~~P"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (fast_tac HOL_cs 1)
         ]);
+*)
 
-
+(* val classical2 = case_split_thm;        "[|Q ==> R; ~Q ==> R|]==>R" *)
+(*
 qed_goal "classical2" HOL.thy "[|Q ==> R; ~Q ==> R|]==>R"
  (fn prems =>
         [
@@ -144,13 +111,17 @@
         (eresolve_tac prems 1),
         (eresolve_tac prems 1)
         ]);
+*)
+(*
+fun case_tac s = res_inst_tac [("Q",s)] classical2;
+*)
 
 
 
 val classical3 = (notE RS notI);
 (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
 
-
+(*
 qed_goal "nat_less_cases" Nat.thy 
     "[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
 ( fn prems =>
@@ -161,10 +132,9 @@
         (etac (sym RS hd (tl prems)) 1),
         (etac (hd prems) 1)
         ]);
-
-
-
+*)
 
-
-
-
+(*
+qed_goal "Suc_less_mono" Nat.thy "Suc n < Suc m = (n < m)" (fn _ => [
+	fast_tac (HOL_cs addIs [Suc_mono] addDs [Suc_less_SucD]) 1]);
+*)
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Holcfb.thy
--- a/src/HOLCF/Holcfb.thy	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Holcfb.thy	Tue Apr 23 17:04:23 1996 +0200
@@ -7,7 +7,9 @@
 
 *)
 
-Holcfb = Nat + 
+Holcfb = Nat 
+
+(* + 
 
 consts
         theleast     :: "(nat=>bool)=>nat"
@@ -15,7 +17,17 @@
 
 theleast_def    "theleast P == (@z.(P z & (!n.P n --> z<=n)))"
 
-(* start 8bit 1 *)
-(* end 8bit 1 *)
+(* start 
+   8bit 1 *)
+
+syntax
+  "Gmu"        :: "[pttrn, bool] => nat"               ("(3´_./ _)" 10)
+
+translations
+  "´x.P"	== "theleast(%x.P)"
+
+(* end
+   8bit 1 *)
 
 end
+*)
\ No newline at end of file
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Lift3.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -306,13 +306,10 @@
         [
         (cut_facts_tac prems 1),
         (rtac allI 1),
-        (rtac (notex2all RS iffD1) 1),
+        (rtac (not_ex RS iffD1) 1),
         (rtac contrapos 1),
         (etac (lift_lemma2 RS iffD1) 2),
-        (rtac notnotI 1),
-        (rtac (chain_UU_I RS spec) 1),
-        (atac 1),
-        (atac 1)
+        (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
         ]);
 
 
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Makefile	Tue Apr 23 17:04:23 1996 +0200
@@ -35,7 +35,7 @@
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/HOLCF:   $(BIN)/HOL  $(FILES) 
 	case "$(COMP)" in \
-	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF;\
+	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
                 if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/HOLCF;\
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Pcpo.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -92,7 +92,7 @@
         (resolve_tac prems 1),
         (rtac ub_rangeI 1),
         (strip_tac 1),
-        (res_inst_tac [("Q","x<i")] classical2 1),
+        (case_tac "x<i" 1),
         (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1),
         (rtac sym 1),
         (fast_tac HOL_cs 1),
@@ -207,7 +207,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac (notall2ex RS iffD1) 1),
+        (rtac (not_all RS iffD1) 1),
         (rtac swap 1),
         (rtac chain_UU_I_inverse 2),
         (etac notnotD 2),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Porder.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -125,7 +125,7 @@
         [
         (cut_facts_tac prems 1),
         (rtac (lub RS ssubst) 1),
-        (etac selectI3 1)
+        (etac (select_eq_Ex RS iffD2) 1)
         ]);
 
 qed_goal "lubE" Porder.thy " M <<| lub(M) ==>  ? x. M <<| x"
@@ -329,7 +329,7 @@
         (cut_facts_tac prems 1),
         (rtac lub_finch1 1),
         (etac conjunct1 1),
-        (rtac selectI3 1),
+        (rtac (select_eq_Ex RS iffD2) 1),
         (etac conjunct2 1)
         ]);
 
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Sprod0.ML
--- a/src/HOLCF/Sprod0.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Sprod0.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -50,7 +50,7 @@
  "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
  (fn prems =>
         [
-        (res_inst_tac [("Q","a=UU|b=UU")] classical2 1),
+        (case_tac "a=UU|b=UU" 1),
         (atac 1),
         (rtac disjI1 1),
         (rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS 
@@ -124,7 +124,7 @@
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac (de_morgan1 RS ssubst) 1),
+        (rtac (de_Morgan_disj RS subst) 1),
         (etac contrapos 1),
         (etac strict_Ispair 1)
         ]);
@@ -148,7 +148,7 @@
         (cut_facts_tac prems 1),
         (rtac contrapos 1),
         (etac defined_Ispair_rev 2),
-        (rtac (de_morgan1 RS iffD1) 1),
+        (rtac (de_Morgan_disj RS iffD2) 1),
         (etac conjI 1),
         (atac 1)
         ]);
@@ -172,7 +172,7 @@
         (rtac conjI 1),
         (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
         (etac arg_cong 1),
-        (rtac (de_morgan1 RS ssubst) 1),
+        (rtac (de_Morgan_disj RS subst) 1),
         (atac 1),
         (rtac disjI1 1),
         (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Sprod3.ML
--- a/src/HOLCF/Sprod3.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Sprod3.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -32,7 +32,7 @@
         (rtac sym 1),
         (rtac lub_chain_maxelem 1),
         (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
-        (rtac (notall2ex RS iffD1) 1),
+        (rtac (not_all RS iffD1) 1),
         (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
         (atac 1),
         (rtac chain_UU_I_inverse 1),
@@ -129,7 +129,7 @@
         (rtac sym 1),
         (rtac lub_chain_maxelem 1),
         (res_inst_tac [("P","%j.Y(j)~=UU")] exE 1),
-        (rtac (notall2ex RS iffD1) 1),
+        (rtac (not_all RS iffD1) 1),
         (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
         (atac 1),
         (rtac chain_UU_I_inverse 1),
@@ -253,13 +253,9 @@
         (rtac strict_Isfst 1),
         (rtac swap 1),
         (etac (defined_IsfstIssnd RS conjunct2) 2),
-        (rtac notnotI 1),
-        (rtac (chain_UU_I RS spec) 1),
-        (rtac (monofun_Issnd RS ch2ch_monofun) 1),
-        (atac 1),
-        (atac 1)
-        ]);
-
+	(fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS 
+				  chain_UU_I RS spec]) 1)
+	]);
 
 qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)"
 (fn prems =>
@@ -281,13 +277,9 @@
         (rtac strict_Issnd 1),
         (rtac swap 1),
         (etac (defined_IsfstIssnd RS conjunct1) 2),
-        (rtac notnotI 1),
-        (rtac (chain_UU_I RS spec) 1),
-        (rtac (monofun_Isfst RS ch2ch_monofun) 1),
-        (atac 1),
-        (atac 1)
-        ]);
-
+        (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS
+				  chain_UU_I RS spec]) 1)
+	]);
 
 qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)"
 (fn prems =>
@@ -663,7 +655,7 @@
         [
         (rtac (beta_cfun RS ssubst) 1),
         (cont_tacR 1),
-        (res_inst_tac [("Q","z=UU")] classical2 1),
+        (case_tac "z=UU" 1),
         (hyp_subst_tac 1),
         (rtac strictify1 1),
         (rtac trans 1),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Ssum0.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -68,13 +68,13 @@
  (fn prems =>
         [
         (rtac conjI 1),
-        (res_inst_tac [("Q","a=UU")] classical2 1),
+        (case_tac "a=UU" 1),
         (atac 1),
         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 
         RS mp RS conjunct1 RS sym) 1),
         (fast_tac HOL_cs 1),
         (atac 1),
-        (res_inst_tac [("Q","b=UU")] classical2 1),
+        (case_tac "b=UU" 1),
         (atac 1),
         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 
         RS mp RS conjunct1 RS sym) 1),
@@ -104,7 +104,7 @@
  "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
  (fn prems =>
         [
-        (res_inst_tac [("Q","a=UU")] classical2 1),
+        (case_tac "a=UU" 1),
         (atac 1),
         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
         RS iffD2 RS mp RS conjunct1 RS sym) 1),
@@ -116,7 +116,7 @@
  "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
  (fn prems =>
         [
-        (res_inst_tac [("Q","b=UU")] classical2 1),
+        (case_tac "b=UU" 1),
         (atac 1),
         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
         RS iffD2 RS mp RS conjunct1 RS sym) 1),
@@ -149,11 +149,11 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("Q","a1=UU")] classical2 1),
+        (case_tac "a1=UU" 1),
         (hyp_subst_tac 1),
         (rtac (inject_Sinl_Rep1 RS sym) 1),
         (etac sym 1),
-        (res_inst_tac [("Q","a2=UU")] classical2 1),
+        (case_tac "a2=UU" 1),
         (hyp_subst_tac 1),
         (etac inject_Sinl_Rep1 1),
         (etac inject_Sinl_Rep2 1),
@@ -166,11 +166,11 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("Q","b1=UU")] classical2 1),
+        (case_tac "b1=UU" 1),
         (hyp_subst_tac 1),
         (rtac (inject_Sinr_Rep1 RS sym) 1),
         (etac sym 1),
-        (res_inst_tac [("Q","b2=UU")] classical2 1),
+        (case_tac "b2=UU" 1),
         (hyp_subst_tac 1),
         (etac inject_Sinr_Rep1 1),
         (etac inject_Sinr_Rep2 1),
@@ -232,7 +232,7 @@
         (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1),
         (etac disjE 1),
         (etac exE 1),
-        (res_inst_tac [("Q","z= Abs_Ssum(Sinl_Rep(UU))")] classical2 1),
+        (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
         (etac disjI1 1),
         (rtac disjI2 1),
         (rtac disjI1 1),
@@ -248,7 +248,7 @@
         (etac arg_cong 1),
         (etac arg_cong 1),
         (etac exE 1),
-        (res_inst_tac [("Q","z= Abs_Ssum(Sinl_Rep(UU))")] classical2 1),
+        (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
         (etac disjI1 1),
         (rtac disjI2 1),
         (rtac disjI2 1),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Ssum2.ML
--- a/src/HOLCF/Ssum2.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Ssum2.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -227,7 +227,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac classical2 1),
+        (rtac case_split_thm 1),
         (etac disjI1 1),
         (rtac disjI2 1),
         (etac ssum_lemma3 1),
@@ -246,7 +246,7 @@
         [
         (cut_facts_tac prems 1),
         (hyp_subst_tac 1),
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (asm_simp_tac Ssum0_ss 1),
         (asm_simp_tac Ssum0_ss 1)
         ]);
@@ -261,7 +261,7 @@
         [
         (cut_facts_tac prems 1),
         (hyp_subst_tac 1),
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (asm_simp_tac Ssum0_ss 1),
         (asm_simp_tac Ssum0_ss 1)
         ]);
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Ssum3.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -24,7 +24,7 @@
         (rtac exI 3),
         (rtac refl 3),
         (etac (monofun_Isinl RS ch2ch_monofun) 2),
-        (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
+        (case_tac "lub(range(Y))=UU" 1),
         (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
         (atac 1),
         (res_inst_tac [("f","Isinl")] arg_cong  1),
@@ -40,7 +40,7 @@
         (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
         (etac (monofun_Isinl RS ch2ch_monofun) 1),
         (rtac allI 1),
-        (res_inst_tac [("Q","Y(k)=UU")] classical2 1),
+        (case_tac "Y(k)=UU" 1),
         (asm_simp_tac Ssum0_ss 1),
         (asm_simp_tac Ssum0_ss 1)
         ]);
@@ -56,7 +56,7 @@
         (rtac exI 3),
         (rtac refl 3),
         (etac (monofun_Isinr RS ch2ch_monofun) 2),
-        (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
+        (case_tac "lub(range(Y))=UU" 1),
         (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
         (atac 1),
         ((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)),
@@ -71,7 +71,7 @@
         (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
         (etac (monofun_Isinr RS ch2ch_monofun) 1),
         (rtac allI 1),
-        (res_inst_tac [("Q","Y(k)=UU")] classical2 1),
+        (case_tac "Y(k)=UU" 1),
         (asm_simp_tac Ssum0_ss 1),
         (asm_simp_tac Ssum0_ss 1)
         ]);
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -40,7 +40,7 @@
 
 val hoare_lemma5 = prove_goal HOLCF.thy 
 "[|(? k. b1`(iterate k g x) ~= TT);\
-\   k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
+\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
 \ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU"
  (fn prems =>
         [
@@ -48,7 +48,7 @@
         (hyp_subst_tac 1),
         (rtac hoare_lemma2 1),
         (etac exE 1),
-        (etac theleast1 1)
+        (etac LeastI 1)
         ]);
 
 val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> b~=TT"
@@ -69,7 +69,7 @@
 
 val hoare_lemma8 = prove_goal HOLCF.thy 
 "[|(? k. b1`(iterate k g x) ~= TT);\
-\   k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
+\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
 \ !m. m < k --> b1`(iterate m g x)=TT"
  (fn prems =>
         [
@@ -81,11 +81,11 @@
         (atac 2),
         (rtac (le_less_trans RS less_irrefl) 1),
         (atac 2),
-        (rtac theleast2 1),
+        (rtac Least_le 1),
         (etac hoare_lemma6 1),
         (rtac (le_less_trans RS less_irrefl) 1),
         (atac 2),
-        (rtac theleast2 1),
+        (rtac Least_le 1),
         (etac hoare_lemma7 1)
         ]);
 
@@ -143,8 +143,8 @@
  (fn prems =>
         [
         (nat_ind_tac "k" 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+        (Simp_tac 1),
+        (Simp_tac 1),
         (strip_tac 1),
         (res_inst_tac [("s","p`(iterate k1 g x)")] trans 1),
         (rtac trans 1),
@@ -152,7 +152,7 @@
         (res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
         (rtac mp 1),
         (etac spec 1),
-        (Simp_tac 1),
+        (simp_tac (!simpset addsimps [less_Suc_eq]) 1),
         (simp_tac HOLCF_ss 1),
         (etac mp 1),
         (strip_tac 1),
@@ -168,24 +168,18 @@
  (fn prems =>
         [
         (nat_ind_tac "k" 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
-        (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+        (Simp_tac 1),
+(simp_tac (!simpset addsimps [less_Suc_eq]) 1),
         (strip_tac 1),
         (res_inst_tac [("s","q`(iterate k1 g x)")] trans 1),
         (rtac trans 1),
         (rtac (q_def3 RS sym) 2),
         (res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
-        (rtac mp 1),
-        (etac spec 1),
-        (Simp_tac 1),
+        (fast_tac HOL_cs 1),
         (simp_tac HOLCF_ss 1),
         (etac mp 1),
         (strip_tac 1),
-        (rtac mp 1),
-        (etac spec 1),
-        (etac less_trans 1),
-        (Simp_tac 1)
-        ]);
+	(fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
 
 (* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
 
@@ -193,14 +187,14 @@
 val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
 (* 
 val hoare_lemma10 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
-    Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
+    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
  p`(iterate ?k3 g ?x1) = p`?x1" : thm
 
 *)
 
 val hoare_lemma11 = prove_goal Hoare.thy 
 "(? n.b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
+\ k=Least(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
 \ --> p`x = iterate k g x"
  (fn prems =>
         [
@@ -214,7 +208,7 @@
         (rtac p_def3 1),
         (asm_simp_tac HOLCF_ss 1),
         (eres_inst_tac
-           [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")] subst 1),
+           [("s","0"),("t","Least(%n. b1`(iterate n g x) ~= TT)")] subst 1),
         (Simp_tac 1),
         (hyp_subst_tac 1),
         (strip_tac 1),
@@ -240,7 +234,7 @@
 
 val hoare_lemma12 = prove_goal Hoare.thy 
 "(? n. b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
+\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
 \ --> p`x = UU"
  (fn prems =>
         [
@@ -398,13 +392,13 @@
 val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
 (* 
 val hoare_lemma25 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
-    Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
+    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
  q`(iterate ?k3 g ?x1) = q`?x1" : thm
 *)
 
 val hoare_lemma26 = prove_goal Hoare.thy 
 "(? n. b1`(iterate n g x)~=TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
+\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
 \ --> q`x = q`(iterate k g x)"
  (fn prems =>
         [
@@ -433,7 +427,7 @@
 
 val hoare_lemma27 = prove_goal Hoare.thy 
 "(? n. b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
+\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
 \ --> q`x = UU"
  (fn prems =>
         [
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/explicit_domains/Coind.ML
--- a/src/HOLCF/explicit_domains/Coind.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Coind.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -84,7 +84,7 @@
         (rewtac stream_bisim_def),
         (strip_tac 1),
         (etac exE 1),
-        (res_inst_tac [("Q","n=UU")] classical2 1),
+        (case_tac "n=UU" 1),
         (rtac disjI1 1),
         (asm_simp_tac (!simpset addsimps coind_rews) 1),
         (rtac disjI2 1),
@@ -112,7 +112,7 @@
         (rtac stream_coind_lemma2 1),
         (strip_tac 1),
         (etac exE 1),
-        (res_inst_tac [("Q","n=UU")] classical2 1),
+        (case_tac "n=UU" 1),
         (asm_simp_tac (!simpset addsimps coind_rews) 1),
         (res_inst_tac [("x","UU::dnat")] exI 1),
         (simp_tac (!simpset addsimps coind_rews addsimps stream_rews) 1),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/explicit_domains/Dlist.ML
--- a/src/HOLCF/explicit_domains/Dlist.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dlist.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -50,7 +50,7 @@
         (cut_facts_tac prems 1),
         (asm_simp_tac (!simpset addsimps 
                 (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (Asm_simp_tac  1),
         (asm_simp_tac (!simpset addsimps [defined_spair]) 1)
         ]);
@@ -229,9 +229,9 @@
         (dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("Q","(x::'a)=UU")] classical2 1),
+        (case_tac "(x::'a)=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("Q","(xl ::'a dlist)=UU")] classical2 1),
+        (case_tac "(xl ::'a dlist)=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1)
         ]);
@@ -255,9 +255,9 @@
 val temp = prove_goal Dlist.thy  "dnil ~= dcons`x`xl"
  (fn prems =>
         [
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("Q","xl=UU")] classical2 1),
+        (case_tac "xl=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (res_inst_tac [("P1","TT = FF")] classical3 1),
         (resolve_tac dist_eq_tr 1),
@@ -345,7 +345,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1)
         ]);
@@ -354,7 +354,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("Q","xl=UU")] classical2 1),
+        (case_tac "xl=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1)
         ]);
@@ -398,10 +398,10 @@
   "dlist_take (Suc n)`(dcons`x`xl)= dcons`x`(dlist_take n`xl)"
  (fn prems =>
         [
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (Asm_simp_tac 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("Q","xl=UU")] classical2 1),
+        (case_tac "xl=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (Asm_simp_tac 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
@@ -498,7 +498,7 @@
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (resolve_tac prems 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("Q","dlist_take n1`xl=UU")] classical2 1),
+        (case_tac "dlist_take n1`xl=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (resolve_tac prems 1),
         (resolve_tac prems 1),
@@ -527,7 +527,7 @@
 qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
  (fn prems =>
         [
-        (res_inst_tac [("Q","l=UU")] classical2 1),
+        (case_tac "l=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
         (etac disjE 1),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/explicit_domains/Dnat.ML
--- a/src/HOLCF/explicit_domains/Dnat.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dnat.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -179,7 +179,7 @@
         (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (res_inst_tac [("Q","n=UU")] classical2 1),
+        (case_tac "n=UU" 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1)
         ]);
@@ -203,7 +203,7 @@
 val temp = prove_goal Dnat.thy   "dzero ~= dsucc`n"
  (fn prems =>
         [
-        (res_inst_tac [("Q","n=UU")] classical2 1),
+        (case_tac "n=UU" 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (res_inst_tac [("P1","TT = FF")] classical3 1),
         (resolve_tac dist_eq_tr 1),
@@ -312,7 +312,7 @@
   "dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)"
  (fn prems =>
         [
-        (res_inst_tac [("Q","xs=UU")] classical2 1),
+        (case_tac "xs=UU" 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (Asm_simp_tac 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
@@ -418,7 +418,7 @@
         (asm_simp_tac (!simpset addsimps dnat_copy) 1),
         (resolve_tac prems 1),
         (asm_simp_tac (!simpset addsimps dnat_copy) 1),
-        (res_inst_tac [("Q","x`xb=UU")] classical2 1),
+        (case_tac "x`xb=UU" 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (resolve_tac prems 1),
         (eresolve_tac prems 1),
@@ -442,7 +442,7 @@
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (resolve_tac prems 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (res_inst_tac [("Q","dnat_take n1`x=UU")] classical2 1),
+        (case_tac "dnat_take n1`x=UU" 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (resolve_tac prems 1),
         (resolve_tac prems 1),
@@ -470,7 +470,7 @@
 qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
  (fn prems =>
         [
-        (res_inst_tac [("Q","s=UU")] classical2 1),
+        (case_tac "s=UU" 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
         (etac disjE 1),
diff -r 33aff4d854e4 -r 36ba4da350c3 src/HOLCF/explicit_domains/Stream.ML
--- a/src/HOLCF/explicit_domains/Stream.ML	Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Stream.ML	Tue Apr 23 17:04:23 1996 +0200
@@ -273,7 +273,7 @@
      "stream_copy`f`(scons`x`xs) = scons`x`(f`xs)"
  (fn prems =>
         [
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (asm_simp_tac (!simpset addsimps stream_rews) 1),
         (asm_simp_tac (!simpset addsimps stream_rews) 1)
         ]);
@@ -281,7 +281,7 @@
 qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
  (fn prems =>
         [
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (asm_simp_tac (!simpset addsimps stream_rews) 1),
         (asm_simp_tac (!simpset addsimps stream_rews) 1)
         ]);
@@ -290,7 +290,7 @@
  "stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
  (fn prems =>
         [
-        (res_inst_tac [("Q","x=UU")] classical2 1),
+        (case_tac "x=UU" 1),
         (asm_simp_tac (!simpset addsimps stream_rews) 1),
         (asm_simp_tac (!simpset addsimps stream_rews) 1)
         ]);
@@ -489,7 +489,7 @@
         (dtac mp 1),
         (atac 1),
         (etac conjE 1),
-        (res_inst_tac [("Q","s1 = UU & s2 = UU")] classical2 1),
+        (case_tac "s1 = UU & s2 = UU" 1),
         (rtac disjI1 1),
         (fast_tac HOL_cs 1),
         (rtac disjI2 1),