# HG changeset patch
# User oheimb
# Date 828548843 -7200
# Node ID aa09de258498c980eb2a5818f95132f553f5565d
# Parent  9b9cdef706695daeb96549403a8d0c01bdddb074
*** empty log message ***

diff -r 9b9cdef70669 -r aa09de258498 src/HOLCF/explicit_domains/Stream.ML
--- a/src/HOLCF/explicit_domains/Stream.ML	Wed Apr 03 14:06:34 1996 +0200
+++ b/src/HOLCF/explicit_domains/Stream.ML	Wed Apr 03 18:27:23 1996 +0200
@@ -311,20 +311,20 @@
 
 fun prover reach defs thm  = prove_goalw Stream.thy defs thm
  (fn prems =>
-        [
-        (res_inst_tac [("t","s1")] (reach RS subst) 1),
-        (res_inst_tac [("t","s2")] (reach RS subst) 1),
-        (rtac (fix_def2 RS ssubst) 1),
-        (rtac (contlub_cfun_fun RS ssubst) 1),
-        (rtac is_chain_iterate 1),
-        (rtac (contlub_cfun_fun RS ssubst) 1),
-        (rtac is_chain_iterate 1),
-        (rtac lub_equal 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac allI 1),
-        (resolve_tac prems 1)
-        ]);
+	[
+	(res_inst_tac [("t","s1")] (reach RS subst) 1),
+	(res_inst_tac [("t","s2")] (reach RS subst) 1),
+	(rtac (fix_def2 RS ssubst) 1),
+	(rtac (contlub_cfun_fun RS ssubst) 1),
+	(rtac is_chain_iterate 1),
+	(rtac (contlub_cfun_fun RS ssubst) 1),
+	(rtac is_chain_iterate 1),
+	(rtac lub_equal 1),
+	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
+	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
+	(rtac allI 1),
+	(resolve_tac prems 1),
+	]);
 
 val stream_take_lemma = prover stream_reach  [stream_take_def]
         "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2";