| Mon, 08 Jan 2018 16:45:30 +0100 |
wenzelm |
prefer qualified names;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:32:59 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 21:43:57 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
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
|
| Mon, 22 Feb 2010 14:11:03 +0100 |
berghofe |
Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 23:19:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 18:43:52 +0200 |
wenzelm |
trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 12:20:43 +0200 |
wenzelm |
qualified Subgoal.FOCUS;
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 22:34:31 +0200 |
wenzelm |
trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 22:28:31 +0200 |
wenzelm |
replaced old METAHYPS by FOCUS;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:49 +0200 |
berghofe |
Terms returned by decomp are now eta-contracted.
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 12:08:48 +0100 |
berghofe |
"prove" function now instantiates relation variable in order
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 02 Aug 2004 10:16:40 +0200 |
ballarin |
Documentation added/improved.
|
file |
diff |
annotate
|
| Tue, 27 Jul 2004 15:39:59 +0200 |
ballarin |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 26 Jul 2004 15:48:50 +0200 |
ballarin |
New prover for transitive and reflexive-transitive closure of relations.
|
file |
diff |
annotate
|