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





Le 19/10/2015 15:07, Rustom Mody a Ãcrit :
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")

Yes, this is an error raised by Isabelle/HOL 2015...

I think that this has been pointed out by some other users of Isabelle. Well, I guess so?

Thomas
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet




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