Tue, 18 Nov 2008 22:25:36 +0100 wenzelm fulfill_proof/thm_proof: commuted lazyness;
Tue, 18 Nov 2008 22:25:30 +0100 wenzelm fulfill_proof/thm_proof: commuted lazyness;
Tue, 18 Nov 2008 21:17:14 +0100 krauss removed lemmas called lemma1 and lemma2
Tue, 18 Nov 2008 18:25:59 +0100 wenzelm force_proofs after cumulative use_thys;
Tue, 18 Nov 2008 18:25:55 +0100 wenzelm signed_string_of_int for priorities;
Tue, 18 Nov 2008 18:25:52 +0100 wenzelm added force_proofs;
Tue, 18 Nov 2008 18:25:49 +0100 wenzelm added force_proofs (based on thms ever passed through enter_thms);
Tue, 18 Nov 2008 18:25:45 +0100 wenzelm tuned;
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;
Tue, 18 Nov 2008 18:25:10 +0100 wenzelm moved table of standard Isabelle symbols to isar-ref manual;
Tue, 18 Nov 2008 18:22:49 +0100 wenzelm added isabelle-implementation manual;
Tue, 18 Nov 2008 13:19:13 +0100 wenzelm disabled threads -- as advertized;
Tue, 18 Nov 2008 11:26:59 +0100 wenzelm changes by Fabian Immler:
Tue, 18 Nov 2008 09:41:23 +0100 ballarin Code for switching to new locales.
Tue, 18 Nov 2008 09:40:44 +0100 ballarin add_thmss
Tue, 18 Nov 2008 09:40:06 +0100 ballarin Activate elements moved to element.ML.
Tue, 18 Nov 2008 00:11:06 +0100 wenzelm finish: force proofs;
Mon, 17 Nov 2008 23:34:35 +0100 wenzelm finish_proof: undefined promises may occur here;
Mon, 17 Nov 2008 23:17:13 +0100 wenzelm tuned promise/fullfill;
Mon, 17 Nov 2008 23:17:11 +0100 wenzelm unified treatment of PAxm/Oracle/Promise in basic proof term operations;
Mon, 17 Nov 2008 21:36:48 +0100 wenzelm removed Induct/Mutil.thy -- the file has been moved to AFP;
Mon, 17 Nov 2008 21:28:46 +0100 wenzelm simplified thm_deps -- no need to build a graph datastructure;
Mon, 17 Nov 2008 21:13:48 +0100 wenzelm removed Induct/Mutil.thy -- the file has been moved to AFP;
Mon, 17 Nov 2008 17:25:02 +0100 nipkow -> AFP
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Mon, 17 Nov 2008 17:00:27 +0100 haftmann explicit name morphism function for locale interpretation
Mon, 17 Nov 2008 17:00:26 +0100 haftmann Name.name_with_prefix (temporarily)
Mon, 17 Nov 2008 17:00:22 +0100 haftmann adjusted locale signature to *_cmd convention
Mon, 17 Nov 2008 17:00:21 +0100 haftmann whitespace tuning
Mon, 17 Nov 2008 14:03:39 +0100 ballarin Generic activation of locales.
Sun, 16 Nov 2008 22:12:44 +0100 wenzelm proof_body/pthm: removed redundant types field;
Sun, 16 Nov 2008 22:12:43 +0100 wenzelm put_name/thm_proof: promises are filled with fulfilled proofs;
Sun, 16 Nov 2008 22:12:41 +0100 wenzelm proof_body/pthm: removed redundant types field;
Sun, 16 Nov 2008 20:03:42 +0100 wenzelm clarified Thm.proof_body_of vs. Thm.proof_of;
Sun, 16 Nov 2008 18:19:27 +0100 berghofe - Corrected order of quantification over Frees.
Sun, 16 Nov 2008 18:18:45 +0100 berghofe Frees in PThms are now quantified in the order of their appearance in the
Sat, 15 Nov 2008 21:31:37 +0100 wenzelm adapted PThm and MinProof;
Sat, 15 Nov 2008 21:31:36 +0100 wenzelm retrieve thm deps from proof_body;
Sat, 15 Nov 2008 21:31:35 +0100 wenzelm retrieve thm deps from proof_body;
Sat, 15 Nov 2008 21:31:32 +0100 wenzelm adapted PThm;
Sat, 15 Nov 2008 21:31:30 +0100 wenzelm proof_of_term: removed obsolete disambiguisation table;
Sat, 15 Nov 2008 21:31:29 +0100 wenzelm rewrite_proof: simplified simprocs (no name required);
Sat, 15 Nov 2008 21:31:27 +0100 wenzelm Thm.proof_of returns proof_body;
Sat, 15 Nov 2008 21:31:25 +0100 wenzelm refined notion of derivation, consiting of promises and proof_body;
Sat, 15 Nov 2008 21:31:23 +0100 wenzelm reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
Sat, 15 Nov 2008 21:31:21 +0100 wenzelm pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
Sat, 15 Nov 2008 21:31:20 +0100 wenzelm ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
Sat, 15 Nov 2008 21:31:19 +0100 wenzelm name_of_thm: Proofterm.fold_proof_atoms;
Sat, 15 Nov 2008 21:31:17 +0100 wenzelm Thm.proof_of returns proof_body;
Sat, 15 Nov 2008 21:31:15 +0100 wenzelm clean: added HOL-Main;
Sat, 15 Nov 2008 21:31:13 +0100 wenzelm rewrite_proof: simplified simprocs (no name required);
Sat, 15 Nov 2008 11:25:17 +0100 wenzelm multithreading support for polyml-5.2 actually disabled -- as advertized;
Fri, 14 Nov 2008 16:49:52 +0100 ballarin Initial part of locale reimplementation.
Fri, 14 Nov 2008 14:00:52 +0100 ballarin Made local_note_prefix public.
Fri, 14 Nov 2008 08:50:11 +0100 haftmann re-educated guess
Fri, 14 Nov 2008 08:50:10 +0100 haftmann namify and name_decl combinators
Fri, 14 Nov 2008 08:50:09 +0100 haftmann Name.is_nothing
Fri, 14 Nov 2008 08:50:08 +0100 haftmann lemmas about dom and minus / insert
Fri, 14 Nov 2008 08:50:07 +0100 haftmann added length_unique operation for code generation
Thu, 13 Nov 2008 22:45:12 +0100 wenzelm updated generated files;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip