| Mon, 05 Nov 2007 22:50:00 +0100 |
kleing |
move itself into HOL types
|
changeset |
files
|
| Mon, 05 Nov 2007 22:49:28 +0100 |
kleing |
rev_nth
|
changeset |
files
|
| Mon, 05 Nov 2007 22:48:37 +0100 |
kleing |
tranclD2 (tranclD at the other end) + trancl_power
|
changeset |
files
|
| Mon, 05 Nov 2007 22:00:21 +0100 |
kleing |
acknowledge authors
|
changeset |
files
|
| Mon, 05 Nov 2007 21:05:03 +0100 |
kleing |
cite Jeremy's avocs article
|
changeset |
files
|
| Mon, 05 Nov 2007 20:50:45 +0100 |
wenzelm |
simplified LocalTheory.reinit;
|
changeset |
files
|
| Mon, 05 Nov 2007 20:50:44 +0100 |
wenzelm |
misc cleanup of init functions;
|
changeset |
files
|
| Mon, 05 Nov 2007 20:50:43 +0100 |
wenzelm |
TheoryTarget.context;
|
changeset |
files
|
| Mon, 05 Nov 2007 20:50:42 +0100 |
wenzelm |
simplified LocalTheory.reinit;
|
changeset |
files
|
| Mon, 05 Nov 2007 20:50:41 +0100 |
wenzelm |
improved error message for missing predicates;
|
changeset |
files
|
| Mon, 05 Nov 2007 18:18:39 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Mon, 05 Nov 2007 17:48:51 +0100 |
ballarin |
Use of export rather than standard in interpretation.
|
changeset |
files
|
| Mon, 05 Nov 2007 17:48:34 +0100 |
ballarin |
Removed inst_morphism'; satisfy_thm avoids compose.
|
changeset |
files
|
| Mon, 05 Nov 2007 17:48:17 +0100 |
ballarin |
Interpretation with named equations.
|
changeset |
files
|
| Mon, 05 Nov 2007 17:48:04 +0100 |
ballarin |
Type instance of thm mk_left_commute in locales.
|
changeset |
files
|