Re: [isabelle] simp only:
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
I guess print_simpset shows the simpset when using simp add:
Can I somehow print the simpset when using simp only: ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and