# HG changeset patch
# User nipkow
# Date 877004041 -7200
# Node ID f6bf42312e9e70727be5551f102dc5d15e454d99
# Parent  7cd00b628e32edc1fb59f38c1acd8b3d3b91fe3c
Simplified proof.

diff -r 7cd00b628e32 -r f6bf42312e9e src/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOLCF/IOA/NTP/Correctness.thy	Thu Oct 16 14:12:58 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.thy	Thu Oct 16 14:14:01 1997 +0200
@@ -12,6 +12,6 @@
 
   hom :: 'm impl_state => 'm list
   "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
-                          else ttl(sq(sen s)))"
+                           else tl(sq(sen s)))"
 
 end
diff -r 7cd00b628e32 -r f6bf42312e9e src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Oct 16 14:12:58 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Oct 16 14:14:01 1997 +0200
@@ -836,11 +836,6 @@
 by (Asm_full_simp_tac 1); 
 (* ~ P a *)
 by (Asm_full_simp_tac 1); 
-by (rtac impI 1);
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1); 
-by (REPEAT (etac conjE 1));
-by (assume_tac 1);
 qed"divide_Seq_lemma";
 
 goal thy "!! x. (x>>xs) << Filter P`y  \