[isabelle] simp only:



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




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