| 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
|
| Wed, 04 Apr 2007 23:29:42 +0200 |
wenzelm |
simplified thy_deps using Theory.ancestors_of (in order of creation);
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:41 +0200 |
wenzelm |
renamed Variable.importT to importT_thms;
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:40 +0200 |
wenzelm |
removed unused dep_graph;
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:39 +0200 |
wenzelm |
theory: maintain ancestors in order of creation;
|
changeset |
files
|