| 2015-10-13 |
haftmann |
2015-10-13 |
prod_case as canonical name for product type eliminator
|
file | diff | annotate |
| 2015-07-05 |
wenzelm |
2015-07-05 |
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-02 |
wenzelm |
2015-06-02 |
clarified context;
|
file | diff | annotate |
| 2015-06-02 |
wenzelm |
2015-06-02 |
clarified context;
|
file | diff | annotate |
| 2015-03-06 |
wenzelm |
2015-03-06 |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file | diff | annotate |
| 2015-03-04 |
wenzelm |
2015-03-04 |
tuned signature -- prefer qualified names;
|
file | diff | annotate |
| 2014-10-29 |
wenzelm |
2014-10-29 |
modernized setup;
|
file | diff | annotate |
| 2014-09-28 |
haftmann |
2014-09-28 |
tuned
|
file | diff | annotate |
| 2013-04-18 |
wenzelm |
2013-04-18 |
simplifier uses proper Proof.context instead of historic type simpset;
|
file | diff | annotate |
| 2011-08-10 |
wenzelm |
2011-08-10 |
old term operations are legacy;
|
file | diff | annotate |
| 2011-06-09 |
wenzelm |
2011-06-09 |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file | diff | annotate |
| 2010-11-06 |
krauss |
2010-11-06 |
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
|
file | diff | annotate |
| 2010-07-01 |
haftmann |
2010-07-01 |
"prod" and "sum" replace "*" and "+" respectively
|
file | diff | annotate |
| 2010-05-28 |
haftmann |
2010-05-28 |
avoid reference to thm PairE
|
file | diff | annotate |
| 2010-05-17 |
wenzelm |
2010-05-17 |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
|
file | diff | annotate |
| 2010-04-30 |
wenzelm |
2010-04-30 |
proper context for rule_by_tactic;
|
file | diff | annotate |
| 2010-02-25 |
wenzelm |
2010-02-25 |
modernized structure Split_Rule;
tuned signature;
more antiquotations;
|
file | diff | annotate |
| 2010-02-07 |
wenzelm |
2010-02-07 |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file | diff | annotate |
| 2009-11-25 |
haftmann |
2009-11-25 |
normalized uncurry take/drop
|
file | diff | annotate |
| 2009-11-24 |
haftmann |
2009-11-24 |
curried take/drop
|
file | diff | annotate |
| 2009-11-01 |
wenzelm |
2009-11-01 |
modernized structure Rule_Cases;
|
file | diff | annotate |
| 2009-07-30 |
haftmann |
2009-07-30 |
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
|
file | diff | annotate |
| 2009-07-29 |
haftmann |
2009-07-29 |
cleaned up abstract tuple operations and named them consistently
|
file | diff | annotate |
| 2009-07-29 |
haftmann |
2009-07-29 |
cleaned up abstract tuple operations and named them consistently
|
file | diff | annotate |
| 2009-03-26 |
wenzelm |
2009-03-26 |
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
|
file | diff | annotate |
| 2009-03-15 |
wenzelm |
2009-03-15 |
simplified attribute setup;
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file | diff | annotate |
| 2008-08-15 |
wenzelm |
2008-08-15 |
Args.name_source(_position) for proper position information;
|
file | diff | annotate |
| 2008-08-09 |
wenzelm |
2008-08-09 |
unified Args.T with OuterLex.token, renamed some operations;
|
file | diff | annotate |
| 2008-06-16 |
wenzelm |
2008-06-16 |
pervasive RuleInsts;
|
file | diff | annotate |
| 2008-06-14 |
wenzelm |
2008-06-14 |
proper context for tactics derived from res_inst_tac;
|
file | diff | annotate |
| 2008-03-20 |
haftmann |
2008-03-20 |
tuned
|
file | diff | annotate |
| 2008-01-26 |
wenzelm |
2008-01-26 |
tuned attribute syntax -- no need for eta-expansion;
|
file | diff | annotate |
| 2007-09-15 |
haftmann |
2007-09-15 |
fixed title
|
file | diff | annotate |
| 2007-02-07 |
berghofe |
2007-02-07 |
Added split_rule attribute.
|
file | diff | annotate |
| 2006-07-11 |
wenzelm |
2006-07-11 |
replaced Term.variant(list) by Name.variant(_list);
|
file | diff | annotate |
| 2006-05-27 |
wenzelm |
2006-05-27 |
complete_split_rule: all Vars;
tuned;
|
file | diff | annotate |
| 2006-01-21 |
wenzelm |
2006-01-21 |
simplified type attribute;
|
file | diff | annotate |
| 2006-01-19 |
wenzelm |
2006-01-19 |
setup: theory -> theory;
|
file | diff | annotate |
| 2006-01-10 |
wenzelm |
2006-01-10 |
Attrib.rule;
|
file | diff | annotate |
| 2005-10-31 |
haftmann |
2005-10-31 |
fold_index replacing foldln
|
file | diff | annotate |
| 2005-04-07 |
wenzelm |
2005-04-07 |
reverted renaming of Some/None in comments and strings;
|
file | diff | annotate |
| 2005-03-04 |
skalberg |
2005-03-04 |
Removed practically all references to Library.foldr.
|
file | diff | annotate |
| 2005-03-03 |
skalberg |
2005-03-03 |
Move towards standard functions.
|
file | diff | annotate |
| 2005-02-13 |
skalberg |
2005-02-13 |
Deleted Library.option type.
|
file | diff | annotate |
| 2004-06-21 |
kleing |
2004-06-21 |
Merged in license change from Isabelle2004
|
file | diff | annotate |
| 2001-10-19 |
wenzelm |
2001-10-19 |
got rid of ML proof scripts for Product_Type;
|
file | diff | annotate |
| 2001-02-03 |
wenzelm |
2001-02-03 |
fixed syntax of 'split_format';
|
file | diff | annotate |
| 2001-02-03 |
wenzelm |
2001-02-03 |
simplified 'split_format' syntax;
|
file | diff | annotate |
| 2001-02-02 |
wenzelm |
2001-02-02 |
module setup;
use hidden internal_split constants;
|
file | diff | annotate |
| 2001-02-01 |
oheimb |
2001-02-01 |
converted to Isar therory, adding attributes complete_split and split_format
|
file | diff | annotate |