--- a/src/HOLCF/explicit_domains/Dlist.ML Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dlist.ML Mon Dec 16 15:04:23 1996 +0100
@@ -8,6 +8,8 @@
open Dlist;
+Delsimps (ex_simps @ all_simps);
+
(* ------------------------------------------------------------------------*)
(* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict *)
(* ------------------------------------------------------------------------*)
@@ -226,7 +228,7 @@
[
(res_inst_tac [("P1","TT << FF")] classical3 1),
(resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(case_tac "(x::'a)=UU" 1),
@@ -244,7 +246,7 @@
(cut_facts_tac prems 1),
(res_inst_tac [("P1","TT << FF")] classical3 1),
(resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1)
@@ -281,11 +283,11 @@
[
(cut_facts_tac prems 1),
(rtac conjI 1),
- (dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dlist_when) 1),
(asm_simp_tac (!simpset addsimps dlist_when) 1),
- (dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dlist_when) 1),
(asm_simp_tac (!simpset addsimps dlist_when) 1)
--- a/src/HOLCF/explicit_domains/Dnat.ML Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.ML Mon Dec 16 15:04:23 1996 +0100
@@ -176,7 +176,7 @@
[
(res_inst_tac [("P1","TT << FF")] classical3 1),
(resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(case_tac "n=UU" 1),
@@ -192,7 +192,7 @@
(cut_facts_tac prems 1),
(res_inst_tac [("P1","TT << FF")] classical3 1),
(resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1)
@@ -228,7 +228,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (dres_inst_tac [("fo5","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1)
--- a/src/HOLCF/explicit_domains/Focus_ex.ML Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Focus_ex.ML Mon Dec 16 15:04:23 1996 +0100
@@ -7,6 +7,8 @@
open Focus_ex;
+ Delsimps (ex_simps @ all_simps);
+
(* first some logical trading *)
val prems = goal Focus_ex.thy
--- a/src/HOLCF/explicit_domains/Stream.ML Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Stream.ML Mon Dec 16 15:04:23 1996 +0100
@@ -53,11 +53,11 @@
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(Asm_simp_tac 1),
(res_inst_tac [("p","y")] upE1 1),
- (contr_tac 1),
+ (contr_tac 1),
(rtac disjI2 1),
(rtac exI 1),
- (rtac exI 1),
(etac conjI 1),
+ (rtac exI 1),
(Asm_simp_tac 1)
]);
@@ -174,11 +174,11 @@
[
(cut_facts_tac prems 1),
(rtac conjI 1),
- (dres_inst_tac [("fo5","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps stream_when) 1),
(asm_simp_tac (!simpset addsimps stream_when) 1),
- (dres_inst_tac [("fo5","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps stream_when) 1),
(asm_simp_tac (!simpset addsimps stream_when) 1)
@@ -323,7 +323,7 @@
(rtac (is_chain_iterate RS ch2ch_fappL) 1),
(rtac (is_chain_iterate RS ch2ch_fappL) 1),
(rtac allI 1),
- (resolve_tac prems 1),
+ (resolve_tac prems 1)
]);
val stream_take_lemma = prover stream_reach [stream_take_def]
@@ -494,7 +494,7 @@
(fast_tac HOL_cs 1),
(rtac disjI2 1),
(rtac disjE 1),
- (etac (de_morgan2 RS ssubst) 1),
+ (etac (de_Morgan_conj RS subst) 1),
(res_inst_tac [("x","shd`s1")] exI 1),
(res_inst_tac [("x","stl`s1")] exI 1),
(res_inst_tac [("x","stl`s2")] exI 1),
@@ -582,19 +582,17 @@
[
(nat_ind_tac "n" 1),
(simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1 ),
- (hyp_subst_tac 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (rtac allI 1),
+ (strip_tac 1),
(res_inst_tac [("s","s2")] streamE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1 ),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (hyp_subst_tac 1),
+ (rotate_tac ~1 1),
+ (asm_full_simp_tac (!simpset addsimps stream_rews) 1),
(subgoal_tac "stream_take n1`xs = xs" 1),
- (rtac ((hd stream_inject) RS conjunct2) 2),
- (atac 4),
- (atac 2),
- (atac 2),
+ (rtac ((hd stream_inject) RS conjunct2) 2),
+ (atac 4),
+ (atac 2),
+ (atac 2),
(rtac cfun_arg_cong 1),
(fast_tac HOL_cs 1)
]);