| Tue, 10 Apr 2007 21:52:38 +0200 |
krauss |
some restructuring
|
changeset |
files
|
| Tue, 10 Apr 2007 21:51:08 +0200 |
huffman |
interpretation bounded_linear_of_real
|
changeset |
files
|
| Tue, 10 Apr 2007 21:50:08 +0200 |
huffman |
removed unnecessary premise from power_le_imp_le_base
|
changeset |
files
|
| Tue, 10 Apr 2007 18:09:58 +0200 |
krauss |
proper handling of morphisms
|
changeset |
files
|
| Tue, 10 Apr 2007 14:11:01 +0200 |
krauss |
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
|
changeset |
files
|
| Tue, 10 Apr 2007 11:55:23 +0200 |
wenzelm |
inline_antiq: no longer forces ML_Syntax.atomic;
|
changeset |
files
|
| Tue, 10 Apr 2007 11:12:55 +0200 |
krauss |
removed dead code
|
changeset |
files
|
| Tue, 10 Apr 2007 11:12:42 +0200 |
krauss |
tuned
|
changeset |
files
|
| Tue, 10 Apr 2007 08:19:20 +0200 |
krauss |
added example for definitions in local contexts
|
changeset |
files
|
| Tue, 10 Apr 2007 08:09:28 +0200 |
krauss |
removed obsolete workaround
|
changeset |
files
|
| Mon, 09 Apr 2007 21:28:24 +0200 |
huffman |
generalized type of lemma setsum_product
|
changeset |
files
|
| Mon, 09 Apr 2007 04:51:28 +0200 |
huffman |
new standard proofs of some LIMSEQ lemmas
|
changeset |
files
|
| Sun, 08 Apr 2007 18:35:19 +0200 |
huffman |
rearranged sections
|
changeset |
files
|
| Sun, 08 Apr 2007 17:54:52 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Sat, 07 Apr 2007 18:54:30 +0200 |
krauss |
removed obsolete workarounds
|
changeset |
files
|