Re: [isabelle] A (very) short Isabelle/HOL tutorial for the functional programmer



On Mon, Oct 19, 2015 at 6:25 PM, Rustom Mody <rustompmody at gmail.com> wrote:

>
> On Mon, Oct 19, 2015 at 2:07 PM, Thomas Genet <thomas.genet at irisa.fr>
> wrote:
>
>>
>> Dear Isabelle users,
>>
>>
>> I wrote a 4 pages Isabelle/HOL tutorial for the functional programmer.
>> It is available here:
>>
>> https://hal.inria.fr/hal-01208577v2
>>
>> Any feedback and comments are welcome.
>>
>>
>
> Thanks for that Thomas!
> Just one point -- I had to change the fun to primrec... Not sure I
> understand why but saw that somewhere and tried
>
>
Well continuing I also get this when I put the first sledgehammer . Is it
expected?

Sledgehammering...
"spass": Try this: apply (simp add: member_rec(2)) (0.0 ms).
"cvc4": Try this: apply (simp add: member_rec(2)) (0.0 ms).
"z3": Try this: apply (simp add: member_rec(2)) (0.0 ms).
"remote_vampire": Internal error:
exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML")



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