src/Pure/Tools/simplifier_trace.ML
2016-09-05 wenzelm 2016-09-05 clarified modules;
2016-04-14 wenzelm 2016-04-14 avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2015-07-17 wenzelm 2015-07-17 tuned;
2014-07-21 wenzelm 2014-07-21 refer to Simplifier Trace panel on first invocation;
2014-07-21 wenzelm 2014-07-21 regular message to refer to Simplifier Trace panel (unused);
2014-07-21 wenzelm 2014-07-21 misc tuning and simplification;
2014-07-21 wenzelm 2014-07-21 clarified "simp_trace_new" and corresponding isar-ref section;
2014-05-21 Lars Hupel 2014-05-21 consolidate "break_thm" and "break_term" attributes into "simp_break";
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-06 Lars Hupel 2014-03-06 tuned
2014-02-19 wenzelm 2014-02-19 removed dead code;
2014-02-18 wenzelm 2014-02-18 proper term equality; proper Args.term_pattern parser (like 'is' or 'let' in Isar);
2014-02-18 wenzelm 2014-02-18 more standard names for protocol and markup elements;
2014-02-18 wenzelm 2014-02-18 tuned whitespace;
2014-02-11 Lars Hupel 2014-02-11 "no_memory" option for the simplifier trace to bypass memoization
2014-02-05 Lars Hupel 2014-02-05 made SML/NJ happy
2014-02-04 Lars Hupel 2014-02-04 interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
2013-12-12 wenzelm 2013-12-12 clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
2013-12-12 wenzelm 2013-12-12 skeleton for Simplifier trace by Lars Hupel;