| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
changeset |
files
|
| Wed, 19 Nov 2008 18:15:31 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 19 Nov 2008 17:55:18 +0100 |
nipkow |
fixed
|
changeset |
files
|
| Wed, 19 Nov 2008 17:54:55 +0100 |
nipkow |
Added new fold operator and renamed the old oe to fold_image.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:04:29 +0100 |
ballarin |
Type inference for elements through syntax module.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:03:13 +0100 |
ballarin |
Use 'if' in connection with 'is_some' and 'the'.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:00:00 +0100 |
ballarin |
Basic types not qualified.
|
changeset |
files
|
| Wed, 19 Nov 2008 16:58:33 +0100 |
ballarin |
Enable switching to new locales during session.
|
changeset |
files
|
| Wed, 19 Nov 2008 08:58:57 +0100 |
haftmann |
explicit inhabitance proof
|
changeset |
files
|
| Tue, 18 Nov 2008 22:25:36 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
changeset |
files
|
| Tue, 18 Nov 2008 22:25:30 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
changeset |
files
|
| Tue, 18 Nov 2008 21:17:14 +0100 |
krauss |
removed lemmas called lemma1 and lemma2
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:59 +0100 |
wenzelm |
force_proofs after cumulative use_thys;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:55 +0100 |
wenzelm |
signed_string_of_int for priorities;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:52 +0100 |
wenzelm |
added force_proofs;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:49 +0100 |
wenzelm |
added force_proofs (based on thms ever passed through enter_thms);
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:42 +0100 |
wenzelm |
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:10 +0100 |
wenzelm |
moved table of standard Isabelle symbols to isar-ref manual;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:22:49 +0100 |
wenzelm |
added isabelle-implementation manual;
|
changeset |
files
|
| Tue, 18 Nov 2008 13:19:13 +0100 |
wenzelm |
disabled threads -- as advertized;
|
changeset |
files
|
| Tue, 18 Nov 2008 11:26:59 +0100 |
wenzelm |
changes by Fabian Immler:
|
changeset |
files
|
| Tue, 18 Nov 2008 09:41:23 +0100 |
ballarin |
Code for switching to new locales.
|
changeset |
files
|
| Tue, 18 Nov 2008 09:40:44 +0100 |
ballarin |
add_thmss
|
changeset |
files
|
| Tue, 18 Nov 2008 09:40:06 +0100 |
ballarin |
Activate elements moved to element.ML.
|
changeset |
files
|
| 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
|
| Sat, 15 Nov 2008 21:31:23 +0100 |
wenzelm |
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:21 +0100 |
wenzelm |
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:20 +0100 |
wenzelm |
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:19 +0100 |
wenzelm |
name_of_thm: Proofterm.fold_proof_atoms;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:17 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:15 +0100 |
wenzelm |
clean: added HOL-Main;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:13 +0100 |
wenzelm |
rewrite_proof: simplified simprocs (no name required);
|
changeset |
files
|