tracing simp

Stream: new members

[Jeremy Teitelbaum]

Can one ask for a report on what theorems simp is applying? Is there a trace option of some kind?

[Eric Rodriguez]

squeeze_simp, simp?, show_term { simp } in preference order :)

[Kevin Buzzard]

Eric's answer is the way to do it, but there are trace options if you're interested (just type them somewhere in your file before the invocation of simp): set_option trace.simplify.rewrite true(to see the theorems simp managed to apply) or set_option trace.simplify true (to see everything it tried).