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