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.
lemma;
authorwenzelm
Wed, 29 Sep 1999 14:39:35 +0200
changeset 7649 ae25e28e5ce9
parent 7648 8258b93cdd32
child 7650 c3e5e85de4c3
lemma;
src/HOL/Isar_examples/W_correct.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Isar_examples/W_correct.thy	Wed Sep 29 14:38:03 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Wed Sep 29 14:39:35 1999 +0200
@@ -32,7 +32,7 @@
     AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
               ==> a |- App e1 e2 :: t1";
 
-theorem has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
+lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
 proof -;
   assume "a |- e :: t";
   thus ?thesis (is "?P a e t");
@@ -142,4 +142,3 @@
 
 
 end;
-
isabelle