Re: [isabelle] Accessing (individual) simplification rules of function definitions



Hi Alexander,

This is also very nice, because one now can refer to the specific rule
as f.name1 and so on. Very helpful.

Many thanks again!

On Fri, Aug 5, 2011 at 3:41 AM, Alexander Krauss <krauss at in.tum.de> wrote:

> On 08/05/2011 12:13 AM, Alfio Martini wrote:
>
>> Great!! Thanks for the quick reply!
>>
>>  f.simps(2)
>>>
>>
> You can also name the rules at definition time:
>
> fun/primrec f :: "..."
> where
>  name1: "..."
> | name2: "..."
>
>
> Alex
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil




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