*To*: Gergely Buday <buday.gergely at uni-eszterhazy.hu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] simp only:*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 15 Jul 2016 09:36:35 +0200*In-reply-to*: <003e01d1de66$a42dcaf0$ec8960d0$@uni-eszterhazy.hu>*References*: <001001d1ddc7$69a95330$3cfbf990$@uni-eszterhazy.hu> <5787C779.50209@inf.ethz.ch> <003e01d1de66$a42dcaf0$ec8960d0$@uni-eszterhazy.hu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Hi Gergely,

Best, Andreas On 15/07/16 09:00, Gergely Buday wrote:

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

**References**:**[isabelle] simp only:***From:*Gergely Buday

**Re: [isabelle] simp only:***From:*Andreas Lochbihler

**Re: [isabelle] simp only:***From:*Gergely Buday

- Previous by Date: Re: [isabelle] simp only:
- Next by Date: [isabelle] Declaration of (co)datatypes (was: Some corrections and amendments)
- Previous by Thread: Re: [isabelle] simp only:
- Next by Thread: [isabelle] Surprise!
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list