Tue, 16 Jul 2002 18:41:50 +0200 |
wenzelm |
export map_context;
|
changeset |
files
|
Tue, 16 Jul 2002 18:41:18 +0200 |
wenzelm |
assert_propT;
|
changeset |
files
|
Tue, 16 Jul 2002 18:41:00 +0200 |
wenzelm |
proper predicate definitions of locale body;
|
changeset |
files
|
Tue, 16 Jul 2002 18:40:11 +0200 |
wenzelm |
add_locale: adapted args;
|
changeset |
files
|
Tue, 16 Jul 2002 18:39:55 +0200 |
wenzelm |
locale: optional predicate name, or "open";
|
changeset |
files
|
Tue, 16 Jul 2002 18:39:27 +0200 |
wenzelm |
module now right after ProofContext (for locales);
|
changeset |
files
|
Tue, 16 Jul 2002 18:38:36 +0200 |
wenzelm |
avoid "_st" versions of proof data;
|
changeset |
files
|
Tue, 16 Jul 2002 18:38:11 +0200 |
wenzelm |
context rules;
|
changeset |
files
|
Tue, 16 Jul 2002 18:37:56 +0200 |
wenzelm |
tuned order of modules;
|
changeset |
files
|
Tue, 16 Jul 2002 18:37:03 +0200 |
wenzelm |
added equal_elim_rule1;
|
changeset |
files
|
Tue, 16 Jul 2002 18:26:52 +0200 |
wenzelm |
moved stuff to List.thy;
|
changeset |
files
|
Tue, 16 Jul 2002 18:26:36 +0200 |
wenzelm |
moved stuff from Main.thy;
|
changeset |
files
|