*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Transfer rule for transfer_forall*From*: Ondřej Kunčar <kuncar at in.tum.de>*Date*: Wed, 13 Mar 2013 16:12:45 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <513F0910.9060806@inf.ethz.ch>*References*: <513DBE7C.7030801@inf.ethz.ch> <513DD413.3030205@in.tum.de> <513E50BD.1040301@in.tum.de> <513F0910.9060806@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/17.0 Thunderbird/17.0

On 03/12/2013 11:53 AM, Andreas Lochbihler wrote:

Dear Ondřej, Thanks a lot for looking into this. It now works fine. But I still don't understand what all these attributes do. In Library/Quotient_List, e.g., list_left_total is declared as reflexivity_rule, but list_right_total as transfer_rule. Is that meant to be that way?

Ondrej

**References**:**[isabelle] Transfer rule for transfer_forall***From:*Andreas Lochbihler

**Re: [isabelle] Transfer rule for transfer_forall***From:*Ondřej Kunčar

**Re: [isabelle] Transfer rule for transfer_forall***From:*Ondřej Kunčar

**Re: [isabelle] Transfer rule for transfer_forall***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] syntax highlighting on stackoverflow
- Next by Date: Re: [isabelle] word wrapping in jEdit output panel
- Previous by Thread: Re: [isabelle] Transfer rule for transfer_forall
- Next by Thread: [isabelle] ARiSVe 2013: submission deadline extension to April 8, 2013
- Cl-isabelle-users March 2013 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