*To*: M A <tesleft at hotmail.com>*Subject*: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 28 Oct 2014 12:31:31 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BAY167-W92FD07BC2D40E96EABAC38B69F0@phx.gbl>*References*: <BAY167-W3024082D992B681F64185DB69E0@phx.gbl> <, > <, > <BAY167-W27953B618A80B2575F3851B69E0@phx.gbl> <, > <, > <, > <16FFFE45-32C8-44B9-8908-A9471D2F4C7D@uibk.ac.at> <, > <, > <BAY167-W1074477050F04D10DA461BBB69E0@phx.gbl> <, > <, > <alpine.LNX.2.00.1410272003580.59545@lxbroy10.informatik.tu-muenchen.de> <, > <BAY167-W1086A25A3C2791880694439B69E0@phx.gbl> <BAY167-W92FD07BC2D40E96EABAC38B69F0@phx.gbl>

I’m afraid that your questions are not very clear. This is partly because of your use of English and partly because you seem to have an unusual application. I think that you will need to find a colleague who can help you express your questions more clearly. Larry Paulson > On 28 Oct 2014, at 08:34, M A <tesleft at hotmail.com> wrote: > > Hi > 1. which libraries are needed to write lemma to find subgoal to observe some functional code?for example, can we import list and complete_lattice or lattice and write associative and distributive lemma and find some subgoals to do functional programming in haskell code for lattice ? > 2. can three lemmas write into one statement by lemma "(A) ^ (B) V (C)" in order to find algorithms for using 3 lemmas by observe the subgoals? > Regards, > Martin

**Follow-Ups**:

**References**:**[isabelle] is it possible to find the function from lemmas and which command can do?***From:*M A

**[isabelle] how to type logical and and logical or operators in Isabelle***From:*M A

**[isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*Makarius

**Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle***From:*M A

**[isabelle] which libraries are needed to help to write lemma for operation in functional programming***From:*M A

- Previous by Date: Re: [isabelle] proof terms & program extraction
- Next by Date: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Previous by Thread: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Next by Thread: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list