| 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
|
| 2011-09-16 |
nipkow |
when applying induction rules, remove names of assumptions that come
|
file |
diff |
annotate
|
| 2011-08-17 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| 2011-06-09 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| 2011-06-09 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| 2011-06-08 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| 2011-04-27 |
wenzelm |
reorganized fixes as specialized (global) name space;
|
file |
diff |
annotate
|
| 2011-04-16 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| 2011-04-08 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| 2010-12-17 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| 2010-08-25 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| 2010-06-24 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| 2010-06-24 |
wenzelm |
tuned auxiliary structures;
|
file |
diff |
annotate
|
| 2010-06-24 |
wenzelm |
Net.encode_type;
|
file |
diff |
annotate
|
| 2010-05-17 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| 2010-04-30 |
wenzelm |
slightly more standard induct_simp_add/del attributes;
|
file |
diff |
annotate
|
| 2010-03-07 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| 2010-03-07 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| 2010-02-27 |
wenzelm |
type/const name: explicitly allow abbreviations as well;
|
file |
diff |
annotate
|
| 2010-02-25 |
wenzelm |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
file |
diff |
annotate
|
| 2010-01-30 |
berghofe |
Added infrastructure for simplifying equality constraints in cases rules.
|
file |
diff |
annotate
|
| 2010-01-10 |
berghofe |
Added infrastructure for simplifying equality constraints.
|
file |
diff |
annotate
|
| 2009-11-25 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| 2009-11-24 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| 2009-11-08 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| 2009-11-01 |
wenzelm |
adapted Item_Net;
|
file |
diff |
annotate
|
| 2009-11-01 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
| 2009-10-29 |
wenzelm |
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
|
file |
diff |
annotate
|
| 2009-10-02 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| 2009-08-28 |
wenzelm |
modernized messages -- eliminated ctyp/cterm operations;
|
file |
diff |
annotate
|
| 2009-07-25 |
wenzelm |
eliminated redundant Library.multiply;
|
file |
diff |
annotate
|
| 2009-07-24 |
wenzelm |
renamed functor InductFun to Induct;
|
file |
diff |
annotate
|
| 2009-07-20 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| 2009-07-17 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
| 2009-03-26 |
wenzelm |
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-17 |
wenzelm |
adapted to general Item_Net;
|
file |
diff |
annotate
|
| 2009-03-15 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
| 2009-03-13 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| 2009-03-13 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| 2009-03-03 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| 2009-01-21 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| 2008-12-31 |
wenzelm |
qualified Term.rename_wrt_term;
|
file |
diff |
annotate
|
| 2008-12-04 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|