Re: [isabelle] Huanhuan Zhang



Dear Mr. 张,

> I usually use "by simp" "by auto" "by arith" in my proof. But I do not know what exactly they mean or what they contains. Can anyone tell me which documents I can read in order to know these? I am now reading Isabelle/HOL a proof assistant for higher order logic and at the same time learn to use Isar.

Some very partial information about the proof methods can be found here:

http://www.cs.miami.edu/~tptp/CASC/J5/SystemDescriptions.html#Isabelle-HOL---2009-2

I hope other readers of the mailing list can complete the information -- e.g., arith is not mentioned.

Regards,

亚斯麦






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