| Tue, 02 Sep 2008 22:41:36 +0200 |
wenzelm |
* Generic Toplevel.add_hook interface allows to analyze the result of
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 20:07:51 +0200 |
wenzelm |
* Result facts now refer to the *full* internal name;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 20:04:26 +0200 |
wenzelm |
* Name bindings in higher specification mechanisms;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 10:28:04 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 29 Aug 2008 07:43:25 +0200 |
haftmann |
dropped parameter prefix for class theorems
|
file |
diff |
annotate
|
| Sat, 23 Aug 2008 23:44:31 +0200 |
wenzelm |
* Isabelle/lib/classes/Pure.jar;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 14:49:53 +0200 |
haftmann |
moved class wellorder to theory Orderings
|
file |
diff |
annotate
|
| Fri, 08 Aug 2008 16:54:33 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 16:41:40 +0200 |
ballarin |
Interpretation command (theory/proof context) no longer simplifies goal.
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 17:50:48 +0200 |
ballarin |
Zorn's Lemma for partial orders.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 16:14:56 +0200 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp];
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 11:02:43 +0200 |
wenzelm |
added command 'linear_undo';
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 11:04:42 +0200 |
haftmann |
unified curried gcd, lcm, zgcd, zlcm
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:03:11 +0200 |
haftmann |
Fract now total; improved code generator setup
|
file |
diff |
annotate
|
| Thu, 10 Jul 2008 13:37:31 +0200 |
wenzelm |
slightly improved @{lemma} (both for latex and ML);
|
file |
diff |
annotate
|
| Fri, 04 Jul 2008 15:57:55 +0200 |
huffman |
HOL-NSA
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 08:19:00 +0200 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 07:58:17 +0200 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 22:58:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 22:56:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 22:54:19 +0200 |
wenzelm |
additional ML antiquotations;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 21:21:13 +0200 |
wenzelm |
@{lemma}: 'by' keyword;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 15:30:46 +0200 |
wenzelm |
ML: improved antiquotations;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 15:31:25 +0200 |
wenzelm |
induct_tac: mutual rules work as for method "induct";
|
file |
diff |
annotate
|