Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
repaired some proofs
authoroheimb
Wed, 18 Dec 1996 13:32:29 +0100
changeset 2439 e73cb5924261
parent 2438 b630fded4566
child 2440 b3ac45aba238
repaired some proofs
src/HOLCF/explicit_domains/Dlist.ML file | annotate | diff | comparison | revisions
src/HOLCF/explicit_domains/Dnat.ML file | annotate | diff | comparison | revisions
src/HOLCF/explicit_domains/Stream.ML file | annotate | diff | comparison | revisions 
--- 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),
--- 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),
--- 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),
isabelle