| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 20:29:53 +0100 |
wenzelm |
tuned: more standard use of order;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 17:15:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 15:12:57 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 13:55:10 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| 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
|