Fri, 23 Nov 2007 21:09:32 +0100 haftmann deleted card definition as code lemma; authentic syntax for card
Fri, 23 Nov 2007 21:09:30 +0100 haftmann separated typedecl module, providing typedecl command with interpretation
Fri, 23 Nov 2007 17:37:56 +0100 paulson faster metis calls
Thu, 22 Nov 2007 14:51:34 +0100 wenzelm tuned; Isabelle2007
Thu, 22 Nov 2007 14:48:52 +0100 wenzelm updated to official Poly/ML 5.1;
Wed, 21 Nov 2007 16:40:51 +0100 wenzelm tuned;
Wed, 21 Nov 2007 16:36:47 +0100 wenzelm include elapsed time for parallel sessions;
Wed, 21 Nov 2007 14:43:50 +0100 wenzelm intern_skolem: disallow qualified names;
Wed, 21 Nov 2007 14:18:23 +0100 haftmann fixed
Wed, 21 Nov 2007 13:42:31 +0100 haftmann dropped diagnostic commands
Tue, 20 Nov 2007 14:01:49 +0100 wenzelm tuned;
Tue, 20 Nov 2007 13:59:23 +0100 wenzelm tuned spacing;
Tue, 20 Nov 2007 13:55:13 +0100 wenzelm updated Proof General advertisement;
Tue, 20 Nov 2007 11:42:15 +0100 wenzelm PolyML.SaveState.loadState: exit on failure;
Mon, 19 Nov 2007 13:42:09 +0100 aspinall Init outer syntax after message setup to avoid spurious output.
Mon, 19 Nov 2007 12:06:10 +0100 isatest update to most recent smlnj version
Mon, 19 Nov 2007 11:09:09 +0100 wenzelm inform_file_processed: made even more robust against bad file specs;
Sun, 18 Nov 2007 16:10:12 +0100 wenzelm removed unused inform_file_processed;
Sun, 18 Nov 2007 16:10:11 +0100 wenzelm init_empty: check before change (avoids non-linear update);
Thu, 15 Nov 2007 18:31:53 +0100 aspinall Add thm_dep preference to menu, inadvertently missed off
Thu, 15 Nov 2007 15:05:03 +0100 wenzelm tuned;
Thu, 15 Nov 2007 13:01:55 +0100 wenzelm use -source instead of -target;
Thu, 15 Nov 2007 11:53:49 +0100 wenzelm target 1.4 of JVM;
Thu, 15 Nov 2007 11:49:04 +0100 wenzelm thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
Thu, 15 Nov 2007 11:49:03 +0100 wenzelm isatool version: clarify that this is the *long* form;
Thu, 15 Nov 2007 11:49:02 +0100 wenzelm ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
Thu, 15 Nov 2007 11:49:00 +0100 wenzelm cover ISABELLE_IDENTIFIER;
Wed, 14 Nov 2007 16:22:44 +0100 wenzelm README for E binary distribution;
Wed, 14 Nov 2007 16:22:32 +0100 wenzelm tuned;
Tue, 13 Nov 2007 18:29:28 +0100 paulson patching in the latest changes from Hurd
Tue, 13 Nov 2007 17:04:16 +0100 wenzelm tuned;
Tue, 13 Nov 2007 16:24:03 +0100 wenzelm some more items;
Tue, 13 Nov 2007 13:51:12 +0100 nipkow updated
Tue, 13 Nov 2007 11:04:30 +0100 berghofe Added JAR paper by Wenzel and Wiedijk.
Tue, 13 Nov 2007 11:02:55 +0100 berghofe Removed some case_names and consumes attributes that are now no longer
Tue, 13 Nov 2007 11:00:29 +0100 berghofe Added TrueE to extraction_expand.
Tue, 13 Nov 2007 10:59:26 +0100 berghofe Added new program extraction examples.
Tue, 13 Nov 2007 10:58:46 +0100 berghofe New case studies for program extraction.
Tue, 13 Nov 2007 10:57:47 +0100 berghofe Moved auxiliary lemmas to separate theory.
Tue, 13 Nov 2007 10:55:54 +0100 berghofe Added new exampes Greatest_Common_Divisor and Euclid.
Tue, 13 Nov 2007 10:55:08 +0100 berghofe Moved nat_eq_dec to Util.thy
Tue, 13 Nov 2007 10:54:40 +0100 berghofe Moved nat_eq_dec and search to Util.thy
Tue, 13 Nov 2007 10:53:39 +0100 berghofe Tuned.
Tue, 13 Nov 2007 10:50:33 +0100 berghofe to_pred and to_set now save induction and case rule tags.
Mon, 12 Nov 2007 23:08:12 +0100 wenzelm removed left-over text links from lynx conversion;
Mon, 12 Nov 2007 21:09:32 +0100 wenzelm back to sigusr2, after Poly/ML 5.1 has been adapted;
Mon, 12 Nov 2007 20:10:34 +0100 wenzelm changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
Mon, 12 Nov 2007 19:02:32 +0100 nipkow updates
Mon, 12 Nov 2007 14:20:21 +0100 haftmann updated
Mon, 12 Nov 2007 11:18:51 +0100 wenzelm reactivated default paragraph formatting for ``proof documents'';
Mon, 12 Nov 2007 11:07:51 +0100 schirmer fixed typo;
Mon, 12 Nov 2007 11:07:22 +0100 schirmer added signatures;
Sun, 11 Nov 2007 20:29:07 +0100 wenzelm abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
Sun, 11 Nov 2007 20:29:06 +0100 wenzelm simplified Consts.dest;
Sun, 11 Nov 2007 20:29:05 +0100 wenzelm simplified Consts.dest;
Sun, 11 Nov 2007 20:29:04 +0100 wenzelm simplified Consts.dest;
Sun, 11 Nov 2007 19:41:26 +0100 nipkow updates
Sun, 11 Nov 2007 17:18:38 +0100 wenzelm avoid ML print in production code;
Sun, 11 Nov 2007 16:58:41 +0100 wenzelm updated;
Sun, 11 Nov 2007 16:50:30 +0100 wenzelm auto quickcheck: reduced messages;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip