# HG changeset patch
# User wenzelm
# Date 1136332360 -3600
# Node ID 05b3f033c72db7ee7121ac84915199095ab4b703
# Parent  48d5419fd191cc599e6d8a44c66ce605e25ac217
removed dead code;

diff -r 48d5419fd191 -r 05b3f033c72d src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Jan 04 00:52:38 2006 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Jan 04 00:52:40 2006 +0100
@@ -988,89 +988,6 @@
 qed"take_lemma_less_induct";
 
 
-(*
-local
-
-fun qnt_tac i (tac, var) = tac THEN res_inst_tac [("x", var)] spec i;
-
-fun add_frees tsig =
-  let
-    fun add (Free (x, T), vars) =
-          if Type.of_sort tsig (T, HOLogic.termS) then x ins vars
-          else vars
-      | add (Abs (_, _, t), vars) = add (t, vars)
-      | add (t $ u, vars) = add (t, add (u, vars))
-      | add (_, vars) = vars;
-   in add end;
-
-
-in
-
-(*Generalizes over all free variables, with the named var outermost.*)
-fun all_frees_tac x i thm =
-  let
-    val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
-    val frees = add_frees tsig (List.nth (prems_of thm, i - 1), [x]);
-    val frees' = sort (op >) (frees \ x) @ [x];
-  in
-    foldl (qnt_tac i) (all_tac, frees') thm
-  end;
-
-end;
-
-
-Goal
-"!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
-\  !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m$(f t h1 h2) = seq_take m$(g t h1 h2);\
-\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \
-\                         ==>   seq_take n$(f (s1 @@ y>>s2) h1 h2) \
-\                             = seq_take n$(g (s1 @@ y>>s2) h1 h2) |] \
-\              ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
-by (strip_tac 1);
-by (resolve_tac seq.take_lemmas 1);
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac [("x","h2a")] spec 1);
-by (res_inst_tac [("x","h1a")] spec 1);
-by (res_inst_tac [("x","x")] spec 1);
-by (rtac nat_less_induct 1);
-by (rtac allI 1);
-by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
-                           simpset())) 1);
-by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
-qed"take_lemma_less_induct";
-
-
-
-Goal
-"!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \
-\        !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m$(f t) = seq_take m$(g t));\
-\                         Forall Q s1; Finite s1; ~ Q y|] \
-\                         ==>   P (seq_take n$(f (s1 @@ y>>s2)) \
-\                                   = seq_take n$(g (s1 @@ y>>s2))) |] \
-\              ==> P ((f x)=(g x))";
-
-by (res_inst_tac [("t","f x = g x"),
-                  ("s","!n. seq_take n$(f x) = seq_take n$(g x)")] subst 1);
-by (rtac seq_take_lemma 1);
-
-wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
-
-
-FIX
-
-by (rtac nat_less_induct 1);
-by (rtac allI 1);
-by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
-                           simpset())) 1);
-by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
-qed"take_lemma_less_induct";
-
-
-*)
-
 
 Goal
 "!! Q. [| A UU  ==> (f UU) = (g UU) ; \