| Tue, 18 Nov 2008 00:11:06 +0100 |
wenzelm |
finish: force proofs;
|
changeset |
files
|
| 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
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
changeset |
files
|
| Sun, 16 Nov 2008 18:19:27 +0100 |
berghofe |
- Corrected order of quantification over Frees.
|
changeset |
files
|
| Sun, 16 Nov 2008 18:18:45 +0100 |
berghofe |
Frees in PThms are now quantified in the order of their appearance in the
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:37 +0100 |
wenzelm |
adapted PThm and MinProof;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:36 +0100 |
wenzelm |
retrieve thm deps from proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:35 +0100 |
wenzelm |
retrieve thm deps from proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:32 +0100 |
wenzelm |
adapted PThm;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:30 +0100 |
wenzelm |
proof_of_term: removed obsolete disambiguisation table;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:29 +0100 |
wenzelm |
rewrite_proof: simplified simprocs (no name required);
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:27 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:25 +0100 |
wenzelm |
refined notion of derivation, consiting of promises and proof_body;
|
changeset |
files
|