Re: [isabelle] simp only:
Andreas Lochbihler wrote:
> 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]].
Still, I am interested in the standard subgoaler and solver. I have found a section for them at
9.3.6 Configurable Simplifier strategies
in the Isabelle/Isar Reference Manual.
In the source, in HOL/Tools/simpdata.ML there is
val HOL_basic_ss =
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps mksimps_pairs)
|> Simplifier.set_mkeqTrue mk_eq_True
|> Simplifier.set_mkcong mk_meta_cong
is this the basic setup for the simplifier in the HOL object logic?
This archive was generated by a fusion of
Pipermail (Mailman edition) and