src/Pure/skip_proof.ML
Sat, 17 Aug 2019 13:24:40 +0200 wenzelm tuned comments;
Sat, 17 Aug 2019 13:16:19 +0200 wenzelm more accurate proposition for cheat_tac (command 'sorry');
Wed, 28 Dec 2016 10:39:50 +0100 wenzelm more uniform treatment of "bad" like other messages (with serial number);
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Fri, 30 Oct 2015 17:14:30 +0100 wenzelm tuned signature -- clarified modules;
Tue, 28 Jul 2015 20:07:05 +0200 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 30 Oct 2014 16:20:46 +0100 wenzelm eliminated aliases;
Sun, 06 Apr 2014 16:36:28 +0200 wenzelm more source positions;
Sun, 06 Apr 2014 15:43:45 +0200 wenzelm more source positions;
Mon, 31 Mar 2014 10:28:08 +0200 wenzelm 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;
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available;
Wed, 27 Mar 2013 14:50:30 +0100 wenzelm clarified Skip_Proof.cheat_tac: more standard tactic;
Wed, 27 Mar 2013 14:19:18 +0100 wenzelm tuned signature and module arrangement;
less more (0) tip