Sat, 22 May 2010 19:17:18 -0700 huffman HOLCF no longer redefines 'consts' command
Sat, 22 May 2010 18:34:38 -0700 huffman for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
Sat, 22 May 2010 17:57:16 -0700 huffman simplify fixrec continuity tactic
Sun, 23 May 2010 22:56:45 +0200 krauss used sledgehammer[isar_proof] to replace slow metis call
Sun, 23 May 2010 17:23:18 +0100 webertj Typo fixed.
Sun, 23 May 2010 17:22:30 +0100 webertj Typo fixed.
Sun, 23 May 2010 14:56:58 +0100 webertj Minor proof tuning.
Sun, 23 May 2010 13:00:01 +0100 webertj Improved document structure.
Sun, 23 May 2010 10:55:01 +0100 webertj Minor proof tuning.
Sun, 23 May 2010 10:38:11 +0100 webertj merged
Sun, 23 May 2010 10:37:43 +0100 webertj Refactoring, minor extensions (e.g., church_rosser).
Sat, 22 May 2010 17:44:12 -0700 huffman NEWS: removed fixrec_simp attribute
Sat, 22 May 2010 16:46:18 -0700 huffman merged
Sat, 22 May 2010 16:45:46 -0700 huffman disambiguate some syntax
Sat, 22 May 2010 14:04:05 -0700 huffman optimize continuity proofs in fixrec package, using cont2cont rules
Sat, 22 May 2010 13:40:15 -0700 huffman add beta_cfun simproc, which uses cont2cont rules
Sat, 22 May 2010 13:27:36 -0700 huffman removed fixrec_simp attribute (cf. a2a1c8a658ef)
Sat, 22 May 2010 12:56:33 -0700 huffman simplify definition of eta_tac
Sat, 22 May 2010 12:36:50 -0700 huffman remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
Sat, 22 May 2010 10:02:07 -0700 huffman remove cont2cont simproc; instead declare cont2cont rules as simp rules
Sat, 22 May 2010 08:30:40 -0700 huffman domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
Sat, 22 May 2010 11:01:59 +0200 haftmann merged
Sat, 22 May 2010 10:13:02 +0200 haftmann modernized sorting algorithms; quicksort implements sort
Sat, 22 May 2010 10:12:50 +0200 haftmann modernized sorting algorithms; quicksort implements sort
Sat, 22 May 2010 10:12:49 +0200 haftmann localized properties_for_sort
Mon, 24 May 2010 23:19:40 +0200 wenzelm @tailrec annotation;
Mon, 24 May 2010 23:01:51 +0200 wenzelm renamed "rev" to "reverse" following usual Scala conventions;
Sat, 22 May 2010 23:59:09 +0200 wenzelm parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
Sat, 22 May 2010 23:53:09 +0200 wenzelm added rev_iterator;
Sat, 22 May 2010 22:30:43 +0200 wenzelm tuned;
Sat, 22 May 2010 22:30:37 +0200 wenzelm access statically typed dockable windows;
Sat, 22 May 2010 22:05:41 +0200 wenzelm simplified dockables using class Dockable;
Sat, 22 May 2010 21:48:01 +0200 wenzelm generic dockable window;
Sat, 22 May 2010 20:59:55 +0200 wenzelm separate event bus and dockable for raw output (stdout);
Sat, 22 May 2010 20:37:59 +0200 wenzelm more Mac OS problems;
Sat, 22 May 2010 20:37:20 +0200 wenzelm ignore system messages;
Sat, 22 May 2010 20:20:51 +0200 wenzelm use proper ISABELLE_PLATFORM instead of adhoc uname;
Sat, 22 May 2010 20:10:11 +0200 wenzelm refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
Sat, 22 May 2010 20:02:26 +0200 wenzelm tuned;
Sat, 22 May 2010 20:00:28 +0200 wenzelm removed timing;
Sat, 22 May 2010 19:42:20 +0200 wenzelm rendering information and style sheets via settings;
Fri, 21 May 2010 23:48:48 +0200 wenzelm more brackets -- unaligned to prevent odd auto-indentation;
Fri, 21 May 2010 23:21:40 +0200 wenzelm merged
Fri, 21 May 2010 17:16:16 +0200 haftmann adjusted to changes in Mapping.thy
Fri, 21 May 2010 15:28:25 +0200 haftmann merged
Fri, 21 May 2010 15:22:37 +0200 haftmann tuned
Fri, 21 May 2010 15:22:37 +0200 haftmann more lemmas about mappings, in particular keys
Fri, 21 May 2010 15:22:36 +0200 haftmann refined
Fri, 21 May 2010 11:50:34 +0200 haftmann nats in Haskell are readable
Fri, 21 May 2010 10:40:59 +0200 Cezary Kaliszyk Let rsp and prs in fun_rel/fun_map format
Fri, 21 May 2010 23:19:27 +0200 wenzelm tuned zoom_box;
Fri, 21 May 2010 22:08:13 +0200 wenzelm print calculation result in the context where the fact is actually defined -- proper externing;
Fri, 21 May 2010 21:28:31 +0200 wenzelm future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
Fri, 21 May 2010 20:46:00 +0200 wenzelm some message styling;
Fri, 21 May 2010 20:10:45 +0200 wenzelm simplified message markup, using plain XML.Elem directly;
Fri, 21 May 2010 18:10:19 +0200 wenzelm more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
Fri, 21 May 2010 17:26:42 +0200 wenzelm refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
Fri, 21 May 2010 16:49:33 +0200 wenzelm bad_result: report fully explicit message;
Fri, 21 May 2010 16:40:25 +0200 wenzelm observe additional isabelle-jedit.css for component and user;
Fri, 21 May 2010 15:29:20 +0200 wenzelm added checkboxes for debug/tracing filter;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip