| Thu, 13 Sep 2007 18:11:59 +0200 |
berghofe |
Generalized equivariance and nominal_inductive commands to
|
changeset |
files
|
| Thu, 13 Sep 2007 18:08:08 +0200 |
berghofe |
Added equivariance lemmas for induct_forall.
|
changeset |
files
|
| Thu, 13 Sep 2007 18:06:50 +0200 |
berghofe |
Added equivariance lemma for induct_implies.
|
changeset |
files
|
| Tue, 11 Sep 2007 14:26:49 +0200 |
webertj |
typo fixed, dead link removed
|
changeset |
files
|
| Mon, 10 Sep 2007 19:21:03 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Mon, 10 Sep 2007 16:09:01 +0200 |
berghofe |
Auto quickcheck now displays counterexample using Proof.goal_message
|
changeset |
files
|
| Sat, 08 Sep 2007 20:37:22 +0200 |
wenzelm |
added String.isSubstring;
|
changeset |
files
|
| Sat, 08 Sep 2007 19:58:39 +0200 |
wenzelm |
export is_finished;
|
changeset |
files
|
| Sat, 08 Sep 2007 19:58:38 +0200 |
wenzelm |
Present.session_name;
|
changeset |
files
|
| Sat, 08 Sep 2007 19:58:37 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 08 Sep 2007 19:58:36 +0200 |
wenzelm |
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
|
changeset |
files
|
| Sat, 08 Sep 2007 19:58:35 +0200 |
wenzelm |
removed thy_ord (erratic due to multi-threading);
|
changeset |
files
|