Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simplified proof.
authornipkow
Thu, 16 Oct 1997 14:14:01 +0200
changeset 3898 f6bf42312e9e
parent 3897 7cd00b628e32
child 3899 41a4abfa60fe
Simplified proof.
src/HOLCF/IOA/NTP/Correctness.thy file | annotate | diff | comparison | revisions
src/HOLCF/IOA/meta_theory/Sequence.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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  \
isabelle