Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] FOLP/simp.ML

view this post on Zulip Email Gateway (Aug 18 2022 at 16:08):

From: Steve W <s.wong.731@gmail.com>
Hi all,

Does FOLP/simp.ML contain the implementation of the simplier used by 'apply
simp'? Or is that only the FOL version of the simplifer?

Thanks
Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 16:08):

From: Tobias Nipkow <nipkow@in.tum.de>
Steve W schrieb:

Hi all,

Does FOLP/simp.ML contain the implementation of the simplier used by 'apply
simp'? Or is that only the FOL version of the simplifer?

As it says in the header of that file: FOLP version of the simplifier.

Tobias

Thanks
Steve

Last updated: Apr 25 2024 at 20:15 UTC