| Thu, 02 Nov 2006 14:27:18 +0100 |
dixon |
bugfix to zipto: left and right were wrong way around.
|
changeset |
files
|
| Thu, 02 Nov 2006 13:35:09 +0100 |
nipkow |
added sum_squared
|
changeset |
files
|
| Wed, 01 Nov 2006 19:07:37 +0100 |
urbanc |
changed a misplaced "also" to a "moreover" (caused a loop somehow)
|
changeset |
files
|
| Wed, 01 Nov 2006 19:03:30 +0100 |
urbanc |
changed to not compile Iteration and Recursion, but Lam_Funs instead
|
changeset |
files
|
| Wed, 01 Nov 2006 17:57:02 +0100 |
huffman |
move DERIV_sumr from Series.thy to Lim.thy
|
changeset |
files
|
| Wed, 01 Nov 2006 17:14:16 +0100 |
huffman |
generalize type of lemma isCont_Id
|
changeset |
files
|
| Wed, 01 Nov 2006 16:48:58 +0100 |
huffman |
new proof of Bseq_NSbseq using transfer
|
changeset |
files
|
| Wed, 01 Nov 2006 16:11:31 +0100 |
urbanc |
changed to use Lam_Funs
|
changeset |
files
|
| Wed, 01 Nov 2006 15:51:11 +0100 |
paulson |
clauses for iff-introduction, unfortunately useless
|
changeset |
files
|
| Wed, 01 Nov 2006 15:50:19 +0100 |
urbanc |
tuned
|
changeset |
files
|
| Wed, 01 Nov 2006 15:49:43 +0100 |
paulson |
Numerous cosmetic changes.
|
changeset |
files
|
| Wed, 01 Nov 2006 15:45:44 +0100 |
urbanc |
not needed anymore
|
changeset |
files
|
| Wed, 01 Nov 2006 15:44:31 +0100 |
urbanc |
these files are superseded by the internal recursion combinator and the file Lam_Funs.thy
|
changeset |
files
|
| Wed, 01 Nov 2006 15:39:20 +0100 |
paulson |
More blacklisting
|
changeset |
files
|
| Wed, 01 Nov 2006 08:46:54 +0100 |
bulwahn |
added lexicographic_order tactic
|
changeset |
files
|
| Tue, 31 Oct 2006 14:59:27 +0100 |
haftmann |
new SML serializer
|
changeset |
files
|
| Tue, 31 Oct 2006 14:59:26 +0100 |
haftmann |
clarified make_term interface
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:23 +0100 |
haftmann |
introduced CodegenData.add_func_legacy
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:16 +0100 |
haftmann |
cleaned up
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:14 +0100 |
haftmann |
adapted seralizer syntax
|
changeset |
files
|
| Tue, 31 Oct 2006 14:58:12 +0100 |
haftmann |
adapted to new serializer syntax
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:18 +0100 |
haftmann |
constructing proof
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:17 +0100 |
haftmann |
dropped constructiv `->
|
changeset |
files
|
| Tue, 31 Oct 2006 09:29:16 +0100 |
haftmann |
new serialization syntax; experimental extensions
|
changeset |
files
|