src/HOLCF/IOA/meta_theory/Sequence.ML

 by (REPEAT(rtac Def_not_UU 1));
 qed"Cons_inject_eq";
 
 Goal "(a>>s<<b>>t) = (a = b & s<<t)";
 by (simp_tac (simpset() addsimps [Consq_def2]) 1);
-by (stac (Def_inject_less_eq RS sym) 1);
+by (simp_tac (simpset() addsimps [seq.inverts]) 1);
+(*by (stac (Def_inject_less_eq RS sym) 1);
 back();
 by (rtac iffI 1);
-(* 1 *)
 by (etac (hd seq.inverts) 1);
 by (REPEAT(rtac Def_not_UU 1));
-(* 2 *)
 by (Asm_full_simp_tac 1);
 by (etac conjE 1);
-by (etac monofun_cfun_arg 1);
+by (etac monofun_cfun_arg 1);*)
 qed"Cons_inject_less_eq";
 
 Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)";
 by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"seq_take_Cons";

 
 section "take_lemma";
 
 Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')";
 by (rtac iffI 1);
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by Auto_tac;
 qed"seq_take_lemma";
 
 Goal
 "  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) \

 \                         ==> ! n. seq_take n$(f (s1 @@ y>>s2)) \
 \                                = seq_take n$(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (case_tac "Forall Q x" 1);
 by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by Auto_tac;
 qed"take_lemma_principle2";
 
 
 (* Note: in the following proofs the ordering of proof steps is very

 \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
 \                         ==>   seq_take (Suc n)$(f (s1 @@ y>>s2)) \
 \                             = seq_take (Suc n)$(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (rtac impI 1);
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
 by (rtac nat_induct 1);
 by (Simp_tac 1);

 \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
 \                         ==>   seq_take n$(f (s1 @@ y>>s2)) \
 \                             = seq_take n$(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (rtac impI 1);
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
 by (rtac nat_less_induct 1);
 by (rtac allI 1);

 \                    A (y>>s) |]   \
 \                    ==>   seq_take (Suc n)$(f (y>>s)) \
 \                        = seq_take (Suc n)$(g (y>>s)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (rtac impI 1);
-by (resolve_tac seq.take_lemmas 1);
+by (resolve_tac [seq.take_lemmas] 1);
 by (rtac mp 1);
 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
 by (rtac nat_induct 1);
 by (Simp_tac 1);