| 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
|
| Sat, 07 Apr 2007 12:40:32 +0200 |
urbanc |
deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
|
changeset |
files
|
| Sat, 07 Apr 2007 11:36:35 +0200 |
urbanc |
tuned slightly the previous commit
|
changeset |
files
|
| Sat, 07 Apr 2007 11:05:25 +0200 |
narboux |
perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
|
changeset |
files
|
| Fri, 06 Apr 2007 01:26:30 +0200 |
huffman |
add new standard proofs for limits of sequences
|
changeset |
files
|
| Thu, 05 Apr 2007 14:56:54 +0200 |
berghofe |
Replaced add_inductive_i by add_inductive_global.
|
changeset |
files
|
| Thu, 05 Apr 2007 14:56:10 +0200 |
berghofe |
- Tried to make name_of_thm more robust against changes of the
|
changeset |
files
|
| Thu, 05 Apr 2007 14:51:28 +0200 |
berghofe |
- Removed occurrences of ProofContext.export in add_ind_def that
|
changeset |
files
|
| Thu, 05 Apr 2007 00:30:32 +0200 |
wenzelm |
thy_deps: sort Context.thy_ord;
|
changeset |
files
|
| Thu, 05 Apr 2007 00:30:31 +0200 |
wenzelm |
added thy_ord -- order of creation;
|
changeset |
files
|