| #
7419dc15 |
|
17-Aug-2019 |
wenzelm <none@none> |
tuned comments;
|
| #
3250cfee |
|
17-Aug-2019 |
wenzelm <none@none> |
more accurate proposition for cheat_tac (command 'sorry');
|
| #
87de1331 |
|
28-Dec-2016 |
wenzelm <none@none> |
more uniform treatment of "bad" like other messages (with serial number);
|
| #
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
| #
7a2fa594 |
|
30-Oct-2015 |
wenzelm <none@none> |
tuned signature -- clarified modules;
|
| #
72987f0d |
|
28-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
ab11590d |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
| #
bced7572 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
| #
92c442b3 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
| #
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;
|
| #
b6e6a472 |
|
26-Mar-2014 |
wenzelm <none@none> |
prefer Context_Position where a context is available;
prefer explicit Context_Position.is_visible -- avoid redundant message composition;
tuned signature;
|
| #
4ce7b0a2 |
|
27-Mar-2013 |
wenzelm <none@none> |
clarified Skip_Proof.cheat_tac: more standard tactic;
clarified Method.cheating: check quick_and_dirty when it is actually applied;
|
| #
c0c9ada8 |
|
27-Mar-2013 |
wenzelm <none@none> |
tuned signature and module arrangement;
--HG--
rename : src/Pure/Isar/skip_proof.ML => src/Pure/skip_proof.ML
|