#
33b23251 |
|
08-Jan-2018 |
wenzelm <none@none> |
prefer qualified names;
|
#
3ff7fdf2 |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
390ebc4a |
|
08-Jun-2011 |
wenzelm <none@none> |
more robust exception pattern General.Subscript;
|
#
d1a2ff7b |
|
16-Apr-2011 |
wenzelm <none@none> |
eliminated old List.nth; tuned;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
dd7c556c |
|
08-Jul-2010 |
haftmann <none@none> |
tuned titles
|
#
4549e8d1 |
|
05-May-2010 |
haftmann <none@none> |
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 =)
|
#
7a2427f5 |
|
27-Oct-2009 |
wenzelm <none@none> |
eliminated some old folds;
|
#
1cc32a22 |
|
26-Oct-2009 |
haftmann <none@none> |
avoid upto if not needed
|
#
50da8ae7 |
|
22-Oct-2009 |
haftmann <none@none> |
map_range (and map_index) combinator
|
#
75401f7b |
|
15-Oct-2009 |
wenzelm <none@none> |
replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
|
#
8e516902 |
|
29-Sep-2009 |
wenzelm <none@none> |
tuned;
|
#
1e5beb93 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
#
894915ec |
|
29-Jul-2009 |
wenzelm <none@none> |
qualified Subgoal.FOCUS;
|
#
f65d489e |
|
26-Jul-2009 |
wenzelm <none@none> |
replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
d647eb14 |
|
01-Mar-2009 |
wenzelm <none@none> |
use long names for old-style fold combinators;
|
#
7b9e1a05 |
|
31-Dec-2008 |
wenzelm <none@none> |
qualified Term.rename_wrt_term;
|
#
62a3ebe2 |
|
07-May-2008 |
berghofe <none@none> |
Terms returned by decomp are now eta-contracted.
|
#
ef2f2984 |
|
24-Sep-2007 |
ballarin <none@none> |
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
|
#
9356c6f2 |
|
18-Sep-2007 |
ballarin <none@none> |
Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
|
#
2cca6f01 |
|
04-Jul-2007 |
wenzelm <none@none> |
avoid polymorphic equality;
|
#
7818c69c |
|
03-Apr-2007 |
wenzelm <none@none> |
removed obsolete sign_of/sign_of_thm;
|
#
a3231234 |
|
11-May-2006 |
wenzelm <none@none> |
avoid raw equality on type thm;
|
#
b8503671 |
|
11-Mar-2006 |
wenzelm <none@none> |
got rid of type Sign.sg;
|
#
d63876a4 |
|
07-Jul-2005 |
obua <none@none> |
1) all theorems in Orderings can now be given as a parameter 2) new function Theory.defs_of 3) new functions Defs.overloading_info and Defs.is_overloaded
|
#
9cc62485 |
|
04-Mar-2005 |
skalberg <none@none> |
Removed practically all references to Library.foldr.
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
f313a2cc |
|
03-Aug-2004 |
ballarin <none@none> |
New transitivity reasoners for transitivity only and quasi orders.
|
#
8350d2f0 |
|
02-Aug-2004 |
ballarin <none@none> |
Documentation added/improved.
|
#
07327d0f |
|
07-Mar-2004 |
ballarin <none@none> |
Bug-fixes for transitivity reasoner.
|
#
29c20de7 |
|
19-Feb-2004 |
ballarin <none@none> |
Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
|