| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 20:57:22 +1000 |
kleing |
print find_thms result in reverse order so best result is on top
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 20:56:12 +1000 |
kleing |
more useful sorting of find_thms results
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 17:57:51 +0200 |
wenzelm |
clarified Query_Operation.register: avoid hard-wired parallel policy;
|
file |
diff |
annotate
|
| Sat, 10 Aug 2013 12:00:34 +0200 |
kleing |
prefer local facts over global ones
|
file |
diff |
annotate
|
| Sat, 10 Aug 2013 11:59:03 +0200 |
kleing |
use local context for name space
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 17:25:47 +0200 |
wenzelm |
enable search in pre-loaded theory;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 16:17:48 +0200 |
wenzelm |
more GUI options;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 15:49:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 15:14:59 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 00:04:47 +0200 |
wenzelm |
more explicit error;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 00:02:18 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 23:52:35 +0200 |
wenzelm |
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 23:34:52 +0200 |
wenzelm |
more robust read_query;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 17:14:02 +0200 |
wenzelm |
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 15:48:13 +0200 |
wenzelm |
more message markup, provided by prover;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 22:46:54 +0200 |
wenzelm |
some actual find_theorems functionality;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 22:17:53 +0200 |
wenzelm |
more general Output.result: allow to update arbitrary properties;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 16:02:06 +0200 |
wenzelm |
minimal print function "find_theorems", which merely echos its arguments;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 23:13:44 +0200 |
wenzelm |
modify background theory where it is actually required (cf. 51dfdcd88e84);
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 22:32:00 +0200 |
wenzelm |
tuned messages -- avoid text folds stemming from Pretty.chunks;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 22:18:20 +0200 |
wenzelm |
proper system options for 'find_theorems';
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 22:00:35 +0200 |
wenzelm |
guard unify tracing via visible status of global theory;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:28:22 +0100 |
wenzelm |
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 10:46:14 +0200 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 12:36:54 +0200 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|