Re: [isabelle] An 'isabelle emacs' wrapper



Am 15.08.2011 00:28, schrieb Tim (McKenzie) Makarios:
> On 12/08/11 23:53, René Neumann wrote:
>> 1.) It can be passed a logic-pattern: This pattern is matched against
>> all logics as returned by `isabelle findlogics` and then the first match
>> is taken:
>> 	So if you have 'HOL HOL-Cava-Libs HOL-Graphs HOL-Library Pure' as
>> images, "C" would match 'HOL-Cava-Libs' as would "L" (first match wins).
> 
> I haven't looked at the script, but wouldn't "L" match 'HOL' first?

Uh - of course. My fault, sorry.

- René





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.