2010-05-23 huffman 2010-05-23 declare a few more cont2cont rules
2010-05-22 huffman 2010-05-22 HOLCF no longer redefines 'consts' command
2010-05-22 huffman 2010-05-22 for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
2010-05-22 huffman 2010-05-22 simplify fixrec continuity tactic
2010-05-23 krauss 2010-05-23 used sledgehammer[isar_proof] to replace slow metis call
2010-05-23 webertj 2010-05-23 Typo fixed.
2010-05-23 webertj 2010-05-23 Typo fixed.
2010-05-23 webertj 2010-05-23 Minor proof tuning.
2010-05-23 webertj 2010-05-23 Improved document structure.
2010-05-23 webertj 2010-05-23 Minor proof tuning.
2010-05-23 webertj 2010-05-23 merged
2010-05-23 webertj 2010-05-23 Refactoring, minor extensions (e.g., church_rosser).
2010-05-22 huffman 2010-05-22 NEWS: removed fixrec_simp attribute
2010-05-22 huffman 2010-05-22 merged
2010-05-22 huffman 2010-05-22 disambiguate some syntax
2010-05-22 huffman 2010-05-22 optimize continuity proofs in fixrec package, using cont2cont rules
2010-05-22 huffman 2010-05-22 add beta_cfun simproc, which uses cont2cont rules
2010-05-22 huffman 2010-05-22 removed fixrec_simp attribute (cf. a2a1c8a658ef)
2010-05-22 huffman 2010-05-22 simplify definition of eta_tac
2010-05-22 huffman 2010-05-22 remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
2010-05-22 huffman 2010-05-22 remove cont2cont simproc; instead declare cont2cont rules as simp rules
2010-05-22 huffman 2010-05-22 domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
2010-05-22 haftmann 2010-05-22 merged
2010-05-22 haftmann 2010-05-22 modernized sorting algorithms; quicksort implements sort
2010-05-22 haftmann 2010-05-22 modernized sorting algorithms; quicksort implements sort
2010-05-22 haftmann 2010-05-22 localized properties_for_sort
2010-05-24 wenzelm 2010-05-24 @tailrec annotation;
2010-05-24 wenzelm 2010-05-24 renamed "rev" to "reverse" following usual Scala conventions;
2010-05-22 wenzelm 2010-05-22 parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
2010-05-22 wenzelm 2010-05-22 added rev_iterator;
2010-05-22 wenzelm 2010-05-22 tuned;
2010-05-22 wenzelm 2010-05-22 access statically typed dockable windows;
2010-05-22 wenzelm 2010-05-22 simplified dockables using class Dockable;
2010-05-22 wenzelm 2010-05-22 generic dockable window;
2010-05-22 wenzelm 2010-05-22 separate event bus and dockable for raw output (stdout);
2010-05-22 wenzelm 2010-05-22 more Mac OS problems;
2010-05-22 wenzelm 2010-05-22 ignore system messages;
2010-05-22 wenzelm 2010-05-22 use proper ISABELLE_PLATFORM instead of adhoc uname;
2010-05-22 wenzelm 2010-05-22 refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
2010-05-22 wenzelm 2010-05-22 tuned;
2010-05-22 wenzelm 2010-05-22 removed timing;
2010-05-22 wenzelm 2010-05-22 rendering information and style sheets via settings; generalized Isabelle_System.try_read; prefer getenv_strict in most situations;
2010-05-21 wenzelm 2010-05-21 more brackets -- unaligned to prevent odd auto-indentation;
2010-05-21 wenzelm 2010-05-21 merged
2010-05-21 haftmann 2010-05-21 adjusted to changes in Mapping.thy
2010-05-21 haftmann 2010-05-21 merged
2010-05-21 haftmann 2010-05-21 tuned
2010-05-21 haftmann 2010-05-21 more lemmas about mappings, in particular keys
2010-05-21 haftmann 2010-05-21 refined
2010-05-21 haftmann 2010-05-21 nats in Haskell are readable
2010-05-21 Cezary Kaliszyk 2010-05-21 Let rsp and prs in fun_rel/fun_map format
2010-05-21 wenzelm 2010-05-21 tuned zoom_box; tuned tooltips;
2010-05-21 wenzelm 2010-05-21 print calculation result in the context where the fact is actually defined -- proper externing; misc tuning;
2010-05-21 wenzelm 2010-05-21 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);
2010-05-21 wenzelm 2010-05-21 some message styling;
2010-05-21 wenzelm 2010-05-21 simplified message markup, using plain XML.Elem directly;
2010-05-21 wenzelm 2010-05-21 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);
2010-05-21 wenzelm 2010-05-21 refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
2010-05-21 wenzelm 2010-05-21 bad_result: report fully explicit message;
2010-05-21 wenzelm 2010-05-21 observe additional isabelle-jedit.css for component and user; visial separation of message divs;