Wed, 30 Sep 2009 23:30:37 +0200 wenzelm Sorts.of_sort_derivation: no pp here;
Wed, 30 Sep 2009 23:28:54 +0200 wenzelm eliminated redundant bindings;
Wed, 30 Sep 2009 23:16:15 +0200 wenzelm actually perform Isar_Document.init on startup;
Wed, 30 Sep 2009 23:13:18 +0200 wenzelm eliminated dead code;
Wed, 30 Sep 2009 22:53:33 +0200 wenzelm removed dead code;
Wed, 30 Sep 2009 22:31:16 +0200 wenzelm handle Type.TYPE_MATCH, not arbitrary exceptions;
Wed, 30 Sep 2009 22:27:20 +0200 wenzelm removed redundant Sign.certify_prop, use Sign.cert_prop instead;
Wed, 30 Sep 2009 22:26:47 +0200 wenzelm PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
Wed, 30 Sep 2009 22:26:25 +0200 wenzelm actually export unit parser;
Wed, 30 Sep 2009 22:25:50 +0200 wenzelm eliminated dead code;
Wed, 30 Sep 2009 22:24:57 +0200 wenzelm eliminated redundant parameters;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Wed, 30 Sep 2009 19:04:48 +0200 haftmann merged
Wed, 30 Sep 2009 17:23:00 +0200 haftmann moved lemmas about sup on bool to Lattices.thy
Wed, 30 Sep 2009 17:16:01 +0200 haftmann moved lemmas about sup on bool to Lattices.thy
Wed, 30 Sep 2009 17:09:06 +0200 haftmann tuned proofs
Wed, 30 Sep 2009 17:04:21 +0200 haftmann tuned headings
Wed, 30 Sep 2009 15:00:43 +0200 wenzelm report unreferenced ids;
Wed, 30 Sep 2009 11:45:42 +0200 wenzelm tuned whitespace;
Wed, 30 Sep 2009 11:36:12 +0200 wenzelm more uniform treatment of structure Unsynchronized in ML bootstrap phase;
Wed, 30 Sep 2009 09:25:18 +0200 haftmann merged
Wed, 30 Sep 2009 08:28:23 +0200 haftmann mandatory prefix where appropriate
Wed, 30 Sep 2009 08:22:07 +0200 haftmann mandatory prefix where appropriate
Wed, 30 Sep 2009 08:21:53 +0200 haftmann tuned whitespace
Wed, 30 Sep 2009 00:57:28 +0200 wenzelm replaced chained_goal by slightly more appropriate flat_goal;
Wed, 30 Sep 2009 00:27:19 +0200 wenzelm made SML/NJ happy;
Wed, 30 Sep 2009 00:17:06 +0200 wenzelm added chained_goal, which presents the goal thm as seen by semi-structured methods;
Tue, 29 Sep 2009 23:19:26 +0200 wenzelm tuned;
Tue, 29 Sep 2009 23:14:57 +0200 wenzelm removed dead/duplicate code;
Tue, 29 Sep 2009 22:53:07 +0200 wenzelm aliases for Thomas Sewell;
Tue, 29 Sep 2009 22:48:24 +0200 wenzelm modernized Balanced_Tree;
Tue, 29 Sep 2009 22:33:27 +0200 wenzelm replaced meta_iffD2 by existing Drule.equal_elim_rule2;
Tue, 29 Sep 2009 21:36:49 +0200 wenzelm tuned header;
Tue, 29 Sep 2009 21:36:33 +0200 wenzelm Thomas Sewell, NICTA: more efficient HOL/record implementation;
Tue, 29 Sep 2009 21:34:59 +0200 wenzelm tuned whitespace -- recover basic Isabelle conventions;
Tue, 29 Sep 2009 18:14:08 +0200 wenzelm merged
Tue, 29 Sep 2009 14:26:33 +1000 Thomas Sewell Merge with isabelle dev changes.
Tue, 29 Sep 2009 14:25:42 +1000 Thomas Sewell Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
Mon, 28 Sep 2009 15:37:19 +1000 Thomas Sewell Avoid a possible variable name conflict in instantiating a theorem.
Mon, 28 Sep 2009 14:16:01 +1000 Thomas Sewell Fix unescaped expressions breaking latex output in Record.thy
Mon, 28 Sep 2009 11:13:11 +1000 Thomas Sewell Merge record patch with updates from isabelle mainline.
Fri, 25 Sep 2009 19:04:18 +1000 Thomas Sewell Avoid record-inner constants in polymorphic definitions in Bali
Thu, 24 Sep 2009 11:33:05 +1000 Thomas Sewell Merge with changes from isabelle dev repository.
Wed, 23 Sep 2009 19:17:48 +1000 tsewell Initial response to feedback from Norbert, Makarius on record patch
Tue, 22 Sep 2009 13:52:19 +1000 Thomas Sewell Branch merge for isabelle mainline updates.
Thu, 17 Sep 2009 14:17:37 +1000 Thomas Sewell Branch merge with updates from mainline isabelle.
Fri, 11 Sep 2009 20:58:29 +1000 Thomas Sewell Implement previous fix (don't duplicate ext_def) correctly.
Fri, 11 Sep 2009 18:03:30 +1000 Thomas Sewell There's no particular reason to duplicate the extension
Fri, 11 Sep 2009 15:57:16 +1000 Thomas Sewell Merged with mainline changes.
Fri, 11 Sep 2009 15:56:51 +1000 Thomas Sewell Adjust some documentation.
Thu, 10 Sep 2009 16:38:18 +1000 Thomas Sewell Simplification of various aspects of the IsTuple component
Thu, 10 Sep 2009 15:18:43 +1000 Thomas Sewell Record patch imported and working.
Thu, 27 Aug 2009 00:40:53 +1000 tsewell Initial attempt at porting record update to repository Isabelle.
Tue, 29 Sep 2009 16:42:29 +0200 wenzelm Synchronized and Unsynchronized;
Tue, 29 Sep 2009 16:42:02 +0200 wenzelm hide "ref" by default, to enforce excplicit indication as Unsynchronized;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Tue, 29 Sep 2009 14:59:24 +0200 wenzelm open_unsynchronized for interactive Isar loop;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Tue, 29 Sep 2009 11:48:32 +0200 wenzelm Raw ML references as unsynchronized state variables.
Mon, 28 Sep 2009 23:51:13 +0200 wenzelm Dummy version of state variables -- plain refs for sequential access.
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip