| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:55:29 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 12:05:11 +0200 |
wenzelm |
simplified type Proof.method;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 21:07:57 +0100 |
wenzelm |
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:44:01 +0100 |
wenzelm |
more uniform check_const/read_const;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
file |
diff |
annotate
|
| 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
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Wed, 17 Jul 2013 13:45:55 +0200 |
wenzelm |
take context from static theory, not dynamic theory certificate;
|
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
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 22:14:27 +0100 |
wenzelm |
Pretty.item markup for improved readability of lists of items;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 20:05:17 +0200 |
wenzelm |
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:00:34 +0100 |
wenzelm |
prefer explicitly qualified exception List.Empty;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 21:51:46 +0100 |
wenzelm |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:51:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 22:21:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 21:39:33 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 20:57:40 +0200 |
wenzelm |
tuned ML style;
|
file |
diff |
annotate
|