| Wed, 01 Jun 2016 10:45:35 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| Thu, 10 Sep 2015 16:44:17 +0200 |
wenzelm |
more standard local_theory operations;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 17:25:36 +0200 |
wenzelm |
tuned -- avoid slightly odd @{cpat};
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
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
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Mon, 23 Feb 2015 14:48:17 +0100 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:47 +0100 |
haftmann |
explicit declaration allows cumulative declaration
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
deleted ineffective declarations
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
dropped unused rules
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
more direct expression of syntactic function records
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
self-contained declaration attribute
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
simpset with no redundancy
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 10:24:16 +0100 |
haftmann |
avoid unused arguments
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 10:24:15 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 10:24:15 +0100 |
haftmann |
more consistent teminology
|
file |
diff |
annotate
|
| Thu, 08 Jan 2015 18:23:27 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 20:10:06 +0100 |
haftmann |
streamlined setup of linear arithmetic
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 20:41:47 +0200 |
wenzelm |
more static simpsets, which also avoids spurious warnings due to duplicate rules provided here;
|
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
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
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, 08 Aug 2011 09:52:09 -0700 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
file |
diff |
annotate
|
| Sun, 24 Oct 2010 20:19:00 +0200 |
nipkow |
nat_number -> eval_nat_numeral
|
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
|