equal
deleted
inserted
replaced
681 |
681 |
682 using [[trace_simp = true]] |
682 using [[trace_simp = true]] |
683 |
683 |
684 Tracing is then active for all invocations of the simplifier in |
684 Tracing is then active for all invocations of the simplifier in |
685 subsequent goal refinement steps. Tracing may also still be enabled or |
685 subsequent goal refinement steps. Tracing may also still be enabled or |
686 disabled via the Proof General settings menu. |
686 disabled via the ProofGeneral settings menu. |
687 |
687 |
688 * Separate commands 'hide_class', 'hide_type', 'hide_const', |
688 * Separate commands 'hide_class', 'hide_type', 'hide_const', |
689 'hide_fact' replace the former 'hide' KIND command. Minor |
689 'hide_fact' replace the former 'hide' KIND command. Minor |
690 INCOMPATIBILITY. |
690 INCOMPATIBILITY. |
691 |
691 |