# HG changeset patch
# User oheimb
# Date 850912349 -3600
# Node ID e73cb5924261bb5b159294f377b11df2038f1060
# Parent  b630fded45662f546c20b9f6382b59e1f5d1d65a
repaired some proofs

diff -r b630fded4566 -r e73cb5924261 src/HOLCF/explicit_domains/Dlist.ML
--- a/src/HOLCF/explicit_domains/Dlist.ML	Wed Dec 18 13:31:47 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dlist.ML	Wed Dec 18 13:32:29 1996 +0100
@@ -190,7 +190,7 @@
 fun prover contr thm = prove_goal Dlist.thy thm
  (fn prems =>
         [
-        (res_inst_tac [("P1",contr)] classical3 1),
+        (res_inst_tac [("P1",contr)] classical2 1),
         (simp_tac (!simpset addsimps dlist_rews) 1),
         (dtac sym 1),
         (Asm_simp_tac  1),
@@ -226,7 +226,7 @@
 val temp = prove_goal Dlist.thy  "~dnil << dcons`(x::'a)`xl"
  (fn prems =>
         [
-        (res_inst_tac [("P1","TT << FF")] classical3 1),
+        (res_inst_tac [("P1","TT << FF")] classical2 1),
         (resolve_tac dist_less_tr 1),
         (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1),
         (etac box_less 1),
@@ -244,7 +244,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("P1","TT << FF")] classical3 1),
+        (res_inst_tac [("P1","TT << FF")] classical2 1),
         (resolve_tac dist_less_tr 1),
         (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1),
         (etac box_less 1),
@@ -261,7 +261,7 @@
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (case_tac "xl=UU" 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("P1","TT = FF")] classical3 1),
+        (res_inst_tac [("P1","TT = FF")] classical2 1),
         (resolve_tac dist_eq_tr 1),
         (dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
         (etac box_equals 1),
diff -r b630fded4566 -r e73cb5924261 src/HOLCF/explicit_domains/Dnat.ML
--- a/src/HOLCF/explicit_domains/Dnat.ML	Wed Dec 18 13:31:47 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.ML	Wed Dec 18 13:32:29 1996 +0100
@@ -141,7 +141,7 @@
 fun prover contr thm = prove_goal Dnat.thy thm
  (fn prems =>
         [
-        (res_inst_tac [("P1",contr)] classical3 1),
+        (res_inst_tac [("P1",contr)] classical2 1),
         (simp_tac (!simpset addsimps dnat_rews) 1),
         (dtac sym 1),
         (Asm_simp_tac  1),
@@ -174,7 +174,7 @@
 val temp = prove_goal Dnat.thy  "~dzero << dsucc`n"
  (fn prems =>
         [
-        (res_inst_tac [("P1","TT << FF")] classical3 1),
+        (res_inst_tac [("P1","TT << FF")] classical2 1),
         (resolve_tac dist_less_tr 1),
         (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
         (etac box_less 1),
@@ -190,7 +190,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("P1","TT << FF")] classical3 1),
+        (res_inst_tac [("P1","TT << FF")] classical2 1),
         (resolve_tac dist_less_tr 1),
         (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
         (etac box_less 1),
@@ -205,7 +205,7 @@
         [
         (case_tac "n=UU" 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (res_inst_tac [("P1","TT = FF")] classical3 1),
+        (res_inst_tac [("P1","TT = FF")] classical2 1),
         (resolve_tac dist_eq_tr 1),
         (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
         (etac box_equals 1),
diff -r b630fded4566 -r e73cb5924261 src/HOLCF/explicit_domains/Stream.ML
--- a/src/HOLCF/explicit_domains/Stream.ML	Wed Dec 18 13:31:47 1996 +0100
+++ b/src/HOLCF/explicit_domains/Stream.ML	Wed Dec 18 13:32:29 1996 +0100
@@ -133,7 +133,7 @@
 fun prover contr thm = prove_goal Stream.thy thm
  (fn prems =>
         [
-        (res_inst_tac [("P1",contr)] classical3 1),
+        (res_inst_tac [("P1",contr)] classical2 1),
         (simp_tac (!simpset addsimps stream_rews) 1),
         (dtac sym 1),
         (Asm_simp_tac 1),
@@ -805,7 +805,7 @@
  (fn prems =>
         [
         (strip_tac 1 ),
-        (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
+        (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical2 1),
         (atac 2),
         (subgoal_tac "!i.stream_finite(Y(i))" 1),
         (fast_tac HOL_cs 1),