Re: [isabelle] simp_trace_new



Isabelle is a logical framework, and that is how quantifier rules are expressed. The declarative representation of quantifier rules in the meta-logic is clearer, I hope, than the common alternative of representing them as computer code.

Larry Paulson


> On 8 Dec 2014, at 14:21, Walther Neuper <wneuper at ist.tugraz.at> wrote:
> 
> ... and seems to give a negative answer to our ultimate question: Can we have a "naive mathematician's approach" to simple quantifier reasoning in Isabelle without delving down to the meta-logic?





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