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.
Removed spurious blank.
authornipkow
Thu, 30 Oct 1997 09:47:26 +0100
changeset 4034 5bb30bedbdc2
parent 4033 43ec35b5054d
child 4035 6ffbc7b11abd
Removed spurious blank. Updated proof because of HOL change.
src/HOLCF/IOA/meta_theory/RefCorrectness.ML file | annotate | diff | comparison | revisions
src/HOLCF/IOA/meta_theory/Sequence.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Oct 30 09:46:11 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Oct 30 09:47:26 1997 +0100
@@ -167,8 +167,6 @@
 
 by (rtac impI 1);
 by (Seq_Finite_induct_tac 1);
-(* base_case *)
-by (fast_tac HOL_cs 1);
 (* main case *)
 by (safe_tac set_cs);
 by (pair_tac "a" 1);
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Oct 30 09:46:11 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Oct 30 09:47:26 1997 +0100
@@ -674,7 +674,7 @@
 by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
 qed"ForallPFilterPid1";
 
-bind_thm(" ForallPFilterPid",ForallPFilterPid1 RS mp);
+bind_thm("ForallPFilterPid",ForallPFilterPid1 RS mp);
 
 
 (* holds also in other direction *)
isabelle