| 2015-09-25 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| 2015-07-26 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| 2015-07-26 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| 2015-07-24 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| 2015-07-05 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| 2015-07-05 |
wenzelm |
eliminated spurious warning/tracing messages -- avoid Display.string_of_thm_without_context;
|
file |
diff |
annotate
|
| 2015-07-05 |
wenzelm |
clarified context;
|
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 |
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-12-21 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2014-11-10 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| 2014-03-21 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| 2011-08-10 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| 2011-04-16 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| 2011-04-08 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| 2010-05-15 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| 2010-05-05 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| 2010-04-30 |
wenzelm |
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| 2010-02-07 |
wenzelm |
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-24 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| 2009-10-29 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| 2009-10-29 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| 2009-10-27 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| 2009-10-22 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| 2009-10-21 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| 2009-10-16 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
| 2009-10-15 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| 2009-09-29 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| 2009-08-29 |
wenzelm |
eliminated hard tabs;
|
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-03-01 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| 2008-12-30 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| 2008-05-18 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| 2008-05-17 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| 2007-09-25 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
| 2007-04-14 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| 2007-04-04 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| 2007-04-03 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
| 2007-02-26 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
| 2006-11-10 |
wenzelm |
tuned Variable.trade;
|
file |
diff |
annotate
|
| 2006-10-20 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| 2006-10-10 |
haftmann |
gen_rem(s) abandoned in favour of remove / subtract
|
file |
diff |
annotate
|
| 2006-07-25 |
wenzelm |
renamed Term.variant_abs to Syntax.variant_abs;
|
file |
diff |
annotate
|
| 2006-06-19 |
wenzelm |
eliminated freeze/varify in favour of Variable.import/export/trade;
|
file |
diff |
annotate
|
| 2006-06-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2006-06-07 |
wenzelm |
do not open Logic;
|
file |
diff |
annotate
|
| 2005-09-12 |
haftmann |
introduced new-style AList operations
|
file |
diff |
annotate
|
| 2005-07-28 |
wenzelm |
Sign.typ_instance;
|
file |
diff |
annotate
|
| 2005-07-19 |
wenzelm |
Logic.incr_tvar;
|
file |
diff |
annotate
|
| 2005-07-13 |
wenzelm |
improved Net interface;
|
file |
diff |
annotate
|
| 2005-03-04 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| 2005-03-03 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| 2005-02-13 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| 2004-05-21 |
wenzelm |
Type.typ_instance;
|
file |
diff |
annotate
|
| 2004-04-22 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2002-05-07 |
wenzelm |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
file |
diff |
annotate
|
| 1999-09-29 |
wenzelm |
Sign.defaultS;
|
file |
diff |
annotate
|