src/HOLCF/Sprod0.ML

 
 qed_goalw "defined_Spair_Rep_rev" Sprod0.thy [Spair_Rep_def]
  "(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 
         conjunct1 RS sym) 1),
         (fast_tac HOL_cs 1),

 qed_goal "strict_Ispair_rev" Sprod0.thy 
         "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
 (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)
         ]);
 
 qed_goalw "defined_Ispair_rev" Sprod0.thy [Ispair_def]

 (fn prems =>
         [
         (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)
         ]);
 
 

         (rtac exI 1),
         (rtac exI 1),
         (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),
         (res_inst_tac [("f","Abs_Sprod")] arg_cong 1),
         (etac trans 1),