Gergely Buday

2016-07-14 12:05:39 UTC

Hi,

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

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