[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Isarmathlib-devel] Function lemma
|
From: |
Slawomir Kolodynski |
|
Subject: |
Re: [Isarmathlib-devel] Function lemma |
|
Date: |
Tue, 17 Jun 2008 14:45:32 -0700 (PDT) |
This is exactly func1_1_L1A from func1.thy
Slawek
--- On Mon, 6/16/08, Sanghyeon Seo <address@hidden> wrote:
> From: Sanghyeon Seo
> Subject: [Isarmathlib-devel] Function lemma
> To: address@hidden
> Date: Monday, June 16, 2008, 8:10 PM
> I tried to prove the following statement, but I can't.
>
> lemma X:
> assumes "f : A -> B" and "ALL x:A.
> f`(x):C"
> shows "f : A -> C"
>
> --
> Seo Sanghyeon
>
>
> _______________________________________________
> Isarmathlib-devel mailing list
> address@hidden
> http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel