2010-05-28 wenzelm 2010-05-28 some updates for release;
2010-05-27 wenzelm 2010-05-27 merged
2010-05-27 boehmes 2010-05-27 added function update examples and set examples
2010-05-27 boehmes 2010-05-27 updated SMT certificates
2010-05-27 boehmes 2010-05-27 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
2010-05-27 boehmes 2010-05-27 merged
2010-05-27 boehmes 2010-05-27 renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-27 boehmes 2010-05-27 made script executable
2010-05-27 boehmes 2010-05-27 use Z3's builtin support for div and mod
2010-05-27 boehmes 2010-05-27 moved SMT into the HOL image
2010-05-27 wenzelm 2010-05-27 slightly odd workaround to ignore markup that is typically displaced;
2010-05-27 wenzelm 2010-05-27 substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up; tuned;
2010-05-27 wenzelm 2010-05-27 further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 misc updates for release;
2010-05-27 wenzelm 2010-05-27 constant Rat.normalize needs to be qualified;
2010-05-27 wenzelm 2010-05-27 merged
2010-05-27 haftmann 2010-05-27 merged
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
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