2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-26 haftmann 2010-05-26 normalized references to constant "split"
2010-05-26 ballarin 2010-05-26 Revise locale test theory layout.
2010-05-26 ballarin 2010-05-26 Merge mixins of distinct interpretations with same base.
2010-05-27 wenzelm 2010-05-27 indicate prospective properties;
2010-05-27 wenzelm 2010-05-27 clarified auto_update vs. update; tuned;
2010-05-27 wenzelm 2010-05-27 more reactive message handling, notably for follow_caret mode; misc tuning and clarification;
2010-05-27 wenzelm 2010-05-27 Command.toString: include id for debugging; Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus; State.+ without side-effect on event bus; Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results; Document_View: tuned commands_changed handling and caret listening; Document_View.selected_command: proper function, not event handler state; Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);
2010-05-26 wenzelm 2010-05-26 merged
2010-05-26 wenzelm 2010-05-26 refer to polyml-5.3.0-old for ppc-darwin;
2010-05-26 boehmes 2010-05-26 try logical and theory abstraction before full abstraction (avoids warnings of linarith)
2010-05-26 boehmes 2010-05-26 updated SMT certificates
2010-05-26 boehmes 2010-05-26 hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns
2010-05-26 haftmann 2010-05-26 more convenient order of code equations
2010-05-26 wenzelm 2010-05-26 misc updates for release;
2010-05-25 wenzelm 2010-05-25 eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-25 wenzelm 2010-05-25 moved ML files where they are actually used; more precise dependencies;
2010-05-25 wenzelm 2010-05-25 renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
2010-05-25 wenzelm 2010-05-25 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
2010-05-25 wenzelm 2010-05-25 eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-25 wenzelm 2010-05-25 tuned -- avoid catch-all exception pattern;
2010-05-25 wenzelm 2010-05-25 updated generated files;
2010-05-25 wenzelm 2010-05-25 merged
2010-05-24 webertj 2010-05-24 merged
2010-05-24 webertj 2010-05-24 Typo fixed.
2010-05-24 huffman 2010-05-24 move HOLCF/Sum_Cpo.thy to HOLCF/Library
2010-05-24 huffman 2010-05-24 move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
2010-05-24 huffman 2010-05-24 move unused pattern match syntax stuff into HOLCF/ex
2010-05-24 huffman 2010-05-24 rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
2010-05-24 haftmann 2010-05-24 more lemmas
2010-05-24 haftmann 2010-05-24 induction and case rules
2010-05-24 ballarin 2010-05-24 Store registrations in efficient data structure.
2010-05-24 ballarin 2010-05-24 Avoid recomputation of registration instance for lookup.
2010-05-24 ballarin 2010-05-24 Consistently use equality for registration lookup.
2010-05-24 ballarin 2010-05-24 Cleaner implementation of sublocale command.
2010-05-24 ballarin 2010-05-24 Reapply mixin patch: base for performance improvements.
2010-05-23 huffman 2010-05-23 merged
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