Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Benchmark suite for Isabelle's `rewrite` tactic

view this post on Zulip Email Gateway (Oct 16 2020 at 08:46):

From: Zack Grannan <>
Hello everyone,

Is there a benchmark suite that tests the rewriting tactic of Isabelle or some
references we can read how it works/performs?

We are implementing a rewrite tactic for Liquid Haskell and it would be great
to compare it with Isabelle's.



view this post on Zulip Email Gateway (Oct 19 2020 at 15:49):

From: Makarius <>
I guess you mean the "simp" family of proof methods, or rather "The
Simplifier" behind it. The isar-ref manual, section 9.3 has many explanations
about it, but you probably need some practical experience with it to see the

It might also help to study the sources:

(You can read Isabelle/Pure sources in the Prover IDE by opening the central
ROOT.ML, which is also in the Documentation panel.)

Various people on this list can probably provide more concrete answers:
high-end users routinely tinker with the Simplifier setup.


Last updated: Jul 15 2022 at 23:21 UTC