| #
8274f3e0 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
| #
d6b5ab04 |
|
05-Sep-2016 |
wenzelm <none@none> |
clarified modules;
--HG--
rename : src/HOL/Tools/value.ML => src/HOL/Tools/value_command.ML
|
| #
70610782 |
|
14-Apr-2016 |
wenzelm <none@none> |
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
|
| #
dccdabe3 |
|
03-Mar-2016 |
wenzelm <none@none> |
clarified modules;
tuned signature;
|
| #
683d6710 |
|
17-Jul-2015 |
wenzelm <none@none> |
tuned;
|
| #
4582d2b7 |
|
21-Jul-2014 |
wenzelm <none@none> |
refer to Simplifier Trace panel on first invocation;
|
| #
ef67ef66 |
|
21-Jul-2014 |
wenzelm <none@none> |
regular message to refer to Simplifier Trace panel (unused);
|
| #
ae418d9f |
|
21-Jul-2014 |
wenzelm <none@none> |
misc tuning and simplification;
|
| #
70f64737 |
|
21-Jul-2014 |
wenzelm <none@none> |
clarified "simp_trace_new" and corresponding isar-ref section;
|
| #
12513f73 |
|
21-May-2014 |
Lars Hupel <lars.hupel@mytum.de> |
consolidate "break_thm" and "break_term" attributes into "simp_break";
--HG--
extra : amend_source : 6e1062171485088e9a593fcf50f596a1373ae6a6
|
| #
16d1cf5d |
|
31-Mar-2014 |
wenzelm <none@none> |
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;
|
| #
fccf7486 |
|
06-Mar-2014 |
Lars Hupel <lars.hupel@mytum.de> |
tuned
|
| #
156998b9 |
|
19-Feb-2014 |
wenzelm <none@none> |
removed dead code;
|
| #
6ad401ff |
|
18-Feb-2014 |
wenzelm <none@none> |
proper term equality;
proper Args.term_pattern parser (like 'is' or 'let' in Isar);
|
| #
93d632dd |
|
18-Feb-2014 |
wenzelm <none@none> |
more standard names for protocol and markup elements;
|
| #
d17e15fd |
|
18-Feb-2014 |
wenzelm <none@none> |
tuned whitespace;
|
| #
823c61a8 |
|
11-Feb-2014 |
Lars Hupel <lars.hupel@mytum.de> |
"no_memory" option for the simplifier trace to bypass memoization
|
| #
f4c7d3c5 |
|
05-Feb-2014 |
Lars Hupel <lars.hupel@mytum.de> |
made SML/NJ happy
|
| #
6b0c03d3 |
|
04-Feb-2014 |
Lars Hupel <lars.hupel@mytum.de> |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
--HG--
extra : amend_source : ecfd76d4e8277199ca35432e0682414689f265fb
|
| #
65c6de1e |
|
12-Dec-2013 |
wenzelm <none@none> |
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
|
| #
14bc13d6 |
|
12-Dec-2013 |
wenzelm <none@none> |
skeleton for Simplifier trace by Lars Hupel;
|