--- 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),