| 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
|
| Fri, 10 Sep 2010 14:37:57 +0200 |
krauss |
improved error message for common mistake (fun f where "g x = ...")
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 15:28:44 +0200 |
krauss |
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
new year's resolution: reindented code in function package
|
file |
diff |
annotate
|
| Mon, 23 Nov 2009 15:05:59 +0100 |
krauss |
eliminated dead code and some unused bindings, reported by polyml
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 14:46:33 +0100 |
wenzelm |
adapted Local_Theory.define -- eliminated odd thm kind;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 22:23:57 +0100 |
krauss |
do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:27:48 +0100 |
wenzelm |
simplified default binding;
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:22:10 +0200 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 22:48:24 +0200 |
wenzelm |
modernized Balanced_Tree;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:32:58 +0200 |
wenzelm |
compare types directly -- no need to invoke Type.eq_type with empty environment;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|