Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_examples/W_correct.thy
changeset 7809 c3e6f27bfcb7
parent 7800 8ee919e42174
child 7968 964b65b4e433 
--- a/src/HOL/Isar_examples/W_correct.thy	Fri Oct 08 16:40:27 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Fri Oct 08 16:47:44 1999 +0200
@@ -143,8 +143,8 @@
           qed;
           show "$ s a |- e2 :: $ u t2";
           proof -;
-            from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2";
-              by blast;
+            from hyp2 W2_ok [RS sym];
+              have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
             hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
               by (rule has_type_subst_closed);
             with s'; show ?thesis; by simp;
isabelle