Sun, 31 May 2015 00:16:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 08 Mar 2015 20:34:53 +0100 |
wenzelm |
misc tuning and simplification;
|
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
|
Fri, 06 Mar 2015 13:39:34 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
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
|
Wed, 28 Jan 2015 14:24:29 +0100 |
eberlm |
Fixed bug in bugfix for function package
|
file |
diff |
annotate
|
Wed, 28 Jan 2015 12:26:56 +0100 |
eberlm |
Fixed variable naming bug in function package
|
file |
diff |
annotate
|
Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 14:21:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 10 Jan 2014 21:37:28 +0100 |
wenzelm |
more elementary management of declared hyps, below structure Assumption;
|
file |
diff |
annotate
|
Sat, 23 Nov 2013 17:07:36 +0100 |
wenzelm |
more accurate goal context;
|
file |
diff |
annotate
|
Mon, 09 Sep 2013 00:14:07 +0200 |
krauss |
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
|
file |
diff |
annotate
|
Sun, 08 Sep 2013 23:58:52 +0200 |
krauss |
clarified
|
file |
diff |
annotate
|
Sun, 08 Sep 2013 23:49:25 +0200 |
krauss |
clarified, dropping unreachable bool special case
|
file |
diff |
annotate
|
Sun, 08 Sep 2013 23:28:27 +0200 |
krauss |
dropped dead code
|
file |
diff |
annotate
|
Sun, 08 Sep 2013 22:32:47 +0200 |
Manuel Eberl |
generate elim rules for elimination of function equalities;
|
file |
diff |
annotate
|
Sun, 16 Jun 2013 22:56:44 +0200 |
krauss |
export dom predicate in the info record
|
file |
diff |
annotate
|
Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
Tue, 13 Mar 2012 20:04:24 +0100 |
wenzelm |
more explicit indication of def names;
|
file |
diff |
annotate
|
Tue, 08 Nov 2011 11:44:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 21:17:47 +0200 |
krauss |
inlined Function_Lib.replace_frees, which is used only once
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Fri, 25 Feb 2011 16:59:48 +0100 |
krauss |
removed support for tail-recursion from function package (now implemented by partial_function)
|
file |
diff |
annotate
|
Sun, 12 Dec 2010 21:41:01 +0100 |
krauss |
tuned headers
|
file |
diff |
annotate
|
Wed, 03 Nov 2010 11:11:49 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 23:45:20 +0200 |
krauss |
some cleanup in Function_Lib
|
file |
diff |
annotate
|
Tue, 28 Sep 2010 12:34:41 +0200 |
krauss |
consolidated tupled_lambda; moved to structure HOLogic
|
file |
diff |
annotate
|