Wed, 21 Sep 2011 22:18:17 +0200 wenzelm alternative Socket_Channel;
Wed, 21 Sep 2011 20:35:50 +0200 wenzelm more abstract wrapping of fifos as System_Channel;
Wed, 21 Sep 2011 17:50:25 +0200 wenzelm slightly more general Socket_IO as part of Pure;
Wed, 21 Sep 2011 16:04:29 +0200 wenzelm more hints on Z3 configuration;
Wed, 21 Sep 2011 15:08:15 +0200 wenzelm reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);
Wed, 21 Sep 2011 07:31:08 +0200 nipkow renamed inv -> filter
Wed, 21 Sep 2011 07:04:04 +0200 nipkow Added proofs about narowing
Wed, 21 Sep 2011 07:03:16 +0200 nipkow added missing makefile dependence
Wed, 21 Sep 2011 06:26:15 +0200 nipkow added example
Wed, 21 Sep 2011 03:24:54 +0200 nipkow tuned
Wed, 21 Sep 2011 02:38:53 +0200 nipkow refined comment
Wed, 21 Sep 2011 09:17:01 +1000 kleing fixed two typos in IMP (by Jean Pichon)
Wed, 21 Sep 2011 00:12:36 +0200 nipkow merged
Tue, 20 Sep 2011 05:48:23 +0200 nipkow Updated IMP to use new induction method
Tue, 20 Sep 2011 05:47:11 +0200 nipkow New proof method "induction" that gives induction hypotheses the name IH.
Tue, 20 Sep 2011 22:11:22 +0200 haftmann official status for UN_singleton
Tue, 20 Sep 2011 21:47:52 +0200 haftmann tuned specification and lemma distribution among theories; tuned proofs
Tue, 20 Sep 2011 15:23:17 +0200 wenzelm more careful treatment of initial update, similar to output panel;
Tue, 20 Sep 2011 15:07:30 +0200 wenzelm proper fact binding;
Tue, 20 Sep 2011 09:30:19 +0200 bulwahn syntactic improvements and tuning names in the code generator due to Florian's code review
Tue, 20 Sep 2011 01:32:04 +0200 krauss match types when applying mono_thm -- previous export generalizes type variables;
Mon, 19 Sep 2011 23:34:22 +0200 wenzelm fixed headers;
Mon, 19 Sep 2011 23:24:32 +0200 wenzelm less ambiguous syntax;
Mon, 19 Sep 2011 23:18:18 +0200 wenzelm tuned proofs;
Mon, 19 Sep 2011 22:48:05 +0200 wenzelm merged
Mon, 19 Sep 2011 16:18:34 +0200 bulwahn catch PatternMatchFail exceptions in narrowing-based quickcheck
Mon, 19 Sep 2011 16:18:33 +0200 bulwahn removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
Mon, 19 Sep 2011 16:18:30 +0200 bulwahn ensuring that some constants are generated in the source code by adding calls in ensure_testable
Mon, 19 Sep 2011 16:18:23 +0200 bulwahn adding abstraction layer; more precise function names
Mon, 19 Sep 2011 16:18:21 +0200 bulwahn adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
Mon, 19 Sep 2011 16:18:19 +0200 bulwahn determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
Mon, 19 Sep 2011 16:18:19 +0200 bulwahn only annotating constants with sort constraints
Mon, 19 Sep 2011 16:18:18 +0200 bulwahn also adding type annotations for the dynamic invocation
Mon, 19 Sep 2011 14:35:51 +0200 noschinl removed legacy lemmas in Complete_Lattices
Mon, 19 Sep 2011 14:24:53 +0200 bulwahn increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling
Mon, 19 Sep 2011 22:45:57 +0200 wenzelm more isatest stats;
Mon, 19 Sep 2011 22:42:57 +0200 wenzelm refined Symbol.is_symbolic -- cover recoded versions as well;
Mon, 19 Sep 2011 22:13:51 +0200 wenzelm double clicks switch to document node buffer;
Mon, 19 Sep 2011 21:53:07 +0200 wenzelm tuned;
Mon, 19 Sep 2011 21:41:48 +0200 wenzelm explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
Mon, 19 Sep 2011 16:40:17 +0200 wenzelm at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
Mon, 19 Sep 2011 14:40:38 +0200 wenzelm instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);
Mon, 19 Sep 2011 14:31:20 +0200 wenzelm unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
Mon, 19 Sep 2011 12:58:52 +0200 wenzelm imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;
Sun, 18 Sep 2011 16:12:43 -0700 huffman merged
Thu, 15 Sep 2011 10:12:36 -0700 huffman numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
Sun, 18 Sep 2011 21:41:36 +0200 wenzelm removed obsolete patches for PG 4.1;
Sun, 18 Sep 2011 21:15:31 +0200 wenzelm additional space for borderless UI;
Sun, 18 Sep 2011 20:26:08 +0200 wenzelm more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);
Sun, 18 Sep 2011 19:49:35 +0200 wenzelm explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
Sun, 18 Sep 2011 16:33:30 +0200 wenzelm isatest settings for macbroy6 (Mac OS X Lion);
Sun, 18 Sep 2011 16:24:26 +0200 wenzelm more Mac OS reference hardware;
Sun, 18 Sep 2011 16:11:26 +0200 wenzelm updated to SML/NJ 110.73;
Sun, 18 Sep 2011 15:59:38 +0200 wenzelm tentative announcement based on current NEWS;
Sun, 18 Sep 2011 15:57:36 +0200 wenzelm tuned;
Sun, 18 Sep 2011 15:39:55 +0200 wenzelm separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
Sun, 18 Sep 2011 15:30:31 +0200 wenzelm updated for release;
Sun, 18 Sep 2011 15:30:21 +0200 wenzelm tuned;
Sun, 18 Sep 2011 14:55:45 +0200 wenzelm updated generated file;
Sun, 18 Sep 2011 14:55:27 +0200 wenzelm updated Complete_Lattices;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip