| Thu, 27 Sep 2007 17:28:05 +0200 |
ballarin |
Fixed setup of transitivity reasoner (function decomp).
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:56:27 +0200 |
ballarin |
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:53:12 +0200 |
ballarin |
Transitivity reasoner set up for locales order and linorder.
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:18 +0200 |
haftmann |
moved class dense_linear_order to Orderings.thy
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:25 +0200 |
haftmann |
moved class ord from Orderings.thy to HOL.thy
|
file |
diff |
annotate
|
| Tue, 19 Jun 2007 23:15:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 19:23:09 +0200 |
haftmann |
tuned boostrap
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 16:57:51 +0200 |
nipkow |
tuned list comprehension, added lemma
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 10:44:28 +0200 |
haftmann |
dropped superfluous name bindings
|
file |
diff |
annotate
|
| Thu, 24 May 2007 08:37:39 +0200 |
haftmann |
rudimentary class target implementation
|
file |
diff |
annotate
|
| Sat, 19 May 2007 14:05:05 +0200 |
nipkow |
unfold min/max in Stefans code generator
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:22 +0200 |
haftmann |
no special treatment in naming of locale predicates stemming form classes
|
file |
diff |
annotate
|