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 =
  empty_simpset @{context}
  setSSolver safe_solver
  setSolver unsafe_solver
  |> Simplifier.set_subgoaler asm_simp_tac
  |> Simplifier.set_mksimps (mksimps mksimps_pairs)
  |> Simplifier.set_mkeqTrue mk_eq_True
  |> Simplifier.set_mkcong mk_meta_cong
  |> simpset_of;

is this the basic setup for the simplifier in the HOL object logic?

- Gergely





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