| Wed, 01 Jun 2016 19:23:18 +0200 |
wenzelm |
more adhoc overloading;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 15:10:27 +0200 |
wenzelm |
prefer rat numberals;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 10:45:35 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 May 2016 21:54:10 +0200 |
wenzelm |
ad-hoc overloading for standard operations on type Rat.rat;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 17:25:36 +0200 |
wenzelm |
tuned -- avoid slightly odd @{cpat};
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
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 22:05:01 +0100 |
wenzelm |
clarified signature;
|
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
|
| Wed, 08 Oct 2014 17:37:20 +0200 |
wenzelm |
eliminated some exotic combinators;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
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
|
| Fri, 22 Jun 2012 15:03:41 +0200 |
huffman |
avoid duplicate simp rules in norm_arith tactic
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 17:22:49 -0700 |
huffman |
avoid warnings
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:04:33 +0100 |
wenzelm |
just one version of fold_rev2;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 20:52:21 +0100 |
wenzelm |
eliminated some clones of eq_list;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:42:40 +0200 |
haftmann |
Table.map replaces Table.map'
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 18:15:50 +0200 |
wenzelm |
removed unused conversions;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 18:12:58 +0200 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 18:11:00 +0200 |
wenzelm |
moved normarith.ML where it is actually used;
|
file |
diff |
annotate
| base
|