| Mon, 17 Nov 2008 23:34:35 +0100 |
wenzelm |
finish_proof: undefined promises may occur here;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:17:13 +0100 |
wenzelm |
tuned promise/fullfill;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:17:11 +0100 |
wenzelm |
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:36:48 +0100 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:28:46 +0100 |
wenzelm |
simplified thm_deps -- no need to build a graph datastructure;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:13:48 +0100 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
changeset |
files
|
| Mon, 17 Nov 2008 17:25:02 +0100 |
nipkow |
-> AFP
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:27 +0100 |
haftmann |
explicit name morphism function for locale interpretation
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:26 +0100 |
haftmann |
Name.name_with_prefix (temporarily)
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:22 +0100 |
haftmann |
adjusted locale signature to *_cmd convention
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:21 +0100 |
haftmann |
whitespace tuning
|
changeset |
files
|
| Mon, 17 Nov 2008 14:03:39 +0100 |
ballarin |
Generic activation of locales.
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:44 +0100 |
wenzelm |
proof_body/pthm: removed redundant types field;
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:43 +0100 |
wenzelm |
put_name/thm_proof: promises are filled with fulfilled proofs;
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:41 +0100 |
wenzelm |
proof_body/pthm: removed redundant types field;
|
changeset |
files
|