| Thu, 12 Dec 2013 22:38:25 +0100 | wenzelm | clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge; | file | diff | annotate |
| Thu, 12 Dec 2013 21:28:13 +0100 | wenzelm | skeleton for Simplifier trace by Lars Hupel; | file | diff | annotate |