| 2016-06-22 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2016-04-12 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| 2016-04-08 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| 2015-12-16 |
wenzelm |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
file |
diff |
annotate
|
| 2015-12-14 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-12-13 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| 2015-09-25 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| 2015-09-09 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| 2015-08-30 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| 2015-07-26 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| 2015-07-05 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| 2015-06-25 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-06-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-06-13 |
wenzelm |
implicit rule for method "cases";
|
file |
diff |
annotate
|
| 2015-05-30 |
wenzelm |
tuned -- more direct Thm.renamed_prop;
|
file |
diff |
annotate
|
| 2015-04-16 |
wenzelm |
discontinued pointless warnings: commands are only defined inside a theory context;
|
file |
diff |
annotate
|
| 2015-04-08 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-04-08 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-04-08 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| 2015-04-06 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|
| 2015-04-06 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| 2015-04-06 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-03-29 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-03-06 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| 2015-03-04 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2015-03-04 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| 2015-02-10 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| 2014-11-26 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| 2014-11-26 |
wenzelm |
added ML antiquotation @{apply n} or @{apply n(k)};
|
file |
diff |
annotate
|
| 2014-11-09 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| 2014-11-09 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| 2014-11-08 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| 2014-11-03 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| 2014-10-30 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| 2014-10-29 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| 2014-08-19 |
wenzelm |
simplified type Proof.method;
|
file |
diff |
annotate
|
| 2014-03-31 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| 2014-03-21 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| 2014-03-20 |
wenzelm |
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
|
file |
diff |
annotate
|
| 2014-03-06 |
wenzelm |
more uniform check_const/read_const;
|
file |
diff |
annotate
|
| 2014-03-06 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
file |
diff |
annotate
|
| 2013-12-14 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| 2013-08-23 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2013-07-27 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| 2013-07-17 |
wenzelm |
take context from static theory, not dynamic theory certificate;
|
file |
diff |
annotate
|
| 2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| 2013-04-09 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| 2013-03-30 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| 2013-03-29 |
wenzelm |
Pretty.item markup for improved readability of lists of items;
|
file |
diff |
annotate
|
| 2012-10-09 |
wenzelm |
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
|
file |
diff |
annotate
|
| 2012-09-29 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| 2012-03-21 |
wenzelm |
prefer explicitly qualified exception List.Empty;
|
file |
diff |
annotate
|
| 2012-03-16 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| 2011-11-06 |
wenzelm |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
|
file |
diff |
annotate
|
| 2011-11-03 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2011-10-16 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
| 2011-10-12 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2011-10-12 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| 2011-10-12 |
wenzelm |
tuned ML style;
|
file |
diff |
annotate
|
| 2011-09-20 |
nipkow |
New proof method "induction" that gives induction hypotheses the name IH.
|
file |
diff |
annotate
|