# HG changeset patch
# User wenzelm
# Date 938608775 -7200
# Node ID ae25e28e5ce941829a0fa6be835a273d4a50e042
# Parent  8258b93cdd329c2e1daa489bed99e76e9dafcb23
lemma;

diff -r 8258b93cdd32 -r ae25e28e5ce9 src/HOL/Isar_examples/W_correct.thy
--- 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;
-