2016-07-14 12:05:39 UTC
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: ?