[isabelle] simp only:



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.