| Sat, 27 Sep 2008 15:20:37 +0200 |
wenzelm |
promise: include check into future body, i.e. joined results are always valid;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:36 +0200 |
wenzelm |
proper transfer of theorems that involve classes being instantiated here;
|
changeset |
files
|
| Sat, 27 Sep 2008 14:26:06 +0200 |
wenzelm |
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
|
changeset |
files
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
changeset |
files
|
| Fri, 26 Sep 2008 17:24:15 +0200 |
wenzelm |
added subset operation;
|
changeset |
files
|
| Fri, 26 Sep 2008 14:53:10 +0200 |
berghofe |
Added fresh_star_const.
|
changeset |
files
|
| Fri, 26 Sep 2008 14:52:27 +0200 |
berghofe |
Added some more theorems to NominalData.
|
changeset |
files
|
| Fri, 26 Sep 2008 14:51:27 +0200 |
berghofe |
Added some more lemmas that are useful in proof of strong induction rule.
|
changeset |
files
|
| Fri, 26 Sep 2008 09:10:02 +0200 |
haftmann |
removed obsolete name convention "func"
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:53 +0200 |
haftmann |
fixed typo
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:52 +0200 |
haftmann |
clarified function transformator interface
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:51 +0200 |
haftmann |
op = vs. eq
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:21 +0200 |
wenzelm |
moved future_scheduler flag to skip_proof.ML;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:20 +0200 |
wenzelm |
added future_scheduler (from thy_info.ML);
|
changeset |
files
|