Thu, 08 Mar 2012 21:36:36 +0100 wenzelm simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
Thu, 08 Mar 2012 21:35:54 +0100 wenzelm tuned;
Thu, 08 Mar 2012 19:56:57 +0100 wenzelm clarified XML signature (again) -- coincide with basic Markup without explicit dependency;
Thu, 08 Mar 2012 17:47:51 +0100 wenzelm more precise warning/error positions;
Wed, 07 Mar 2012 23:21:00 +0100 wenzelm merged
Wed, 07 Mar 2012 21:38:29 +0100 haftmann less rigorous but more realistic migration recommendation; note on code generation of sets
Wed, 07 Mar 2012 21:34:36 +0100 haftmann tuned syntax; more candidates
Wed, 07 Mar 2012 23:21:24 +0100 wenzelm tuned message (cf. ML version);
Wed, 07 Mar 2012 20:49:18 +0100 wenzelm eliminated dead code;
Wed, 07 Mar 2012 19:38:36 +0100 wenzelm tuned signature;
Wed, 07 Mar 2012 19:32:52 +0100 wenzelm simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode);
Wed, 07 Mar 2012 16:13:49 +0100 berghofe to_pred/set attributes now properly handle variables of type "... => T set"
Wed, 07 Mar 2012 14:30:35 +0100 wenzelm some recovery of IsaMakefile targets from f3c10e908f65;
Wed, 07 Mar 2012 13:00:30 +0000 sultana added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
Wed, 07 Mar 2012 13:00:30 +0000 sultana added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
Wed, 07 Mar 2012 13:00:30 +0000 sultana added Mirabelle action info in its log file; tuned;
Tue, 06 Mar 2012 17:01:37 +0000 paulson More mathematical symbols for ZF examples
Tue, 06 Mar 2012 16:46:27 +0000 paulson mathematical symbols for Isabelle/ZF example theories
Tue, 06 Mar 2012 16:06:52 +0000 paulson Using mathematical notation for <-> and cardinal arithmetic
Tue, 06 Mar 2012 15:15:49 +0000 paulson mathematical symbols instead of ASCII
Sun, 04 Mar 2012 23:20:43 +0100 blanchet addressed a quotient-type-related issue that arose with the port to "set"
Sun, 04 Mar 2012 23:20:43 +0100 blanchet ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
Sun, 04 Mar 2012 23:04:40 +0100 wenzelm updates for jedit-4.5.0 (still inactive);
Sun, 04 Mar 2012 21:46:22 +0100 wenzelm more explicit patches;
Sun, 04 Mar 2012 19:24:05 +0100 wenzelm tuned comment;
Sun, 04 Mar 2012 19:16:09 +0100 wenzelm removed obsolete proper_command_at (cf. 03a2dc9e0624);
Sun, 04 Mar 2012 19:03:28 +0100 wenzelm added Command.proper_range (still unused);
Sun, 04 Mar 2012 18:15:45 +0100 wenzelm clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
Sun, 04 Mar 2012 16:02:14 +0100 wenzelm clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
Sun, 04 Mar 2012 11:03:10 +0100 haftmann tuned
Sun, 04 Mar 2012 10:34:44 +0100 haftmann move test targets to test target
Sun, 04 Mar 2012 10:33:47 +0100 haftmann dropped images for importer sessions
Sun, 04 Mar 2012 00:29:19 +0100 haftmann dropped dead code
Sun, 04 Mar 2012 00:27:07 +0100 haftmann more accurate dependencies
Sun, 04 Mar 2012 00:26:23 +0100 haftmann tuned ML
Sun, 04 Mar 2012 00:17:13 +0100 haftmann dropped silly code
Sun, 04 Mar 2012 00:15:08 +0100 haftmann tuned
Sun, 04 Mar 2012 00:04:37 +0100 haftmann dropped dead code
Sun, 04 Mar 2012 00:03:21 +0100 haftmann actually add "the" Importer theory
Sun, 04 Mar 2012 00:03:04 +0100 haftmann avoid internal hol4 name references in generic importer code
Sat, 03 Mar 2012 23:54:44 +0100 haftmann generalized user-visible text
Sat, 03 Mar 2012 23:49:54 +0100 haftmann generalized attribute name
Sat, 03 Mar 2012 23:49:22 +0100 haftmann dropped dead theories
Sat, 03 Mar 2012 23:43:21 +0100 haftmann one unified Importer theory
Sat, 03 Mar 2012 23:42:56 +0100 haftmann added actual dependencies
Sat, 03 Mar 2012 23:18:23 +0100 haftmann import all importer theories in compatibility layer
Sat, 03 Mar 2012 22:53:24 +0100 wenzelm merged;
Sat, 03 Mar 2012 22:46:34 +0100 haftmann dropped obsolete ROOT.ML
Sat, 03 Mar 2012 22:38:53 +0100 haftmann plugged in pre-existing theories appropriately
Sat, 03 Mar 2012 22:38:33 +0100 haftmann switch of target Import-HOL_Light-Imported: not operative at the moment
Sat, 03 Mar 2012 22:38:11 +0100 haftmann turn on quick and dirty in batch mode
Sat, 03 Mar 2012 22:37:56 +0100 haftmann tuned whitespace
Sat, 03 Mar 2012 22:37:41 +0100 haftmann file system structure separating HOL4 and HOL Light concerns
Sat, 03 Mar 2012 21:51:38 +0100 haftmann distribution of compatibility theories
Sat, 03 Mar 2012 21:42:41 +0100 haftmann formal infrastructure for import sessions
Sat, 03 Mar 2012 21:01:32 +0100 haftmann dropped dead code
Sat, 03 Mar 2012 21:01:23 +0100 haftmann tuned whitespace
Sat, 03 Mar 2012 21:00:31 +0100 haftmann spurious set/pred correction
Sat, 03 Mar 2012 21:00:24 +0100 haftmann explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction
Sat, 03 Mar 2012 21:00:04 +0100 haftmann explicit locations for import_theory and setup_theory, for better user interface conformance
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip