Re: [isabelle] simp only:

Hi Gergely,

There's no need to print it. "simp only:" clears all the simpset, so there are no rewrite rules in there, but all the subgoalers and solvers remain as is. If you specify some rewrite rules, then these will be the only ones in the simpset. If you want to find out how the simplifier preprocesses theses rules, you can look at the trace with [[simp_trace]].

Hope this helps,

On 14/07/16 14:01, Gergely Buday wrote:

The Isabelle/Isar Reference Manual says about simp only:

Implicit solvers remain, which means that trivial rules like reflexivity or

introduction of True are available to solve the simplified subgoals, but

also non-trivial tools like linear arithmetic in HOL. The latter may lead

to some surprise of the meaning of âonlyâ in Isabelle/HOL compared

to English!

I guess print_simpset shows the simpset when using simp add:

Can I somehow print the simpset when using simp only: ?

- Gergely

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