| #
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.
|