2010-05-28 ago wenzelm reuse main view.font from jEdit;
2010-05-28 ago wenzelm deleted some old fonts;
2010-05-28 ago wenzelm also set font for printing, which actually works out of the box;
2010-05-28 ago wenzelm lib/Tools/makeall does not hardiwre logics;
2010-05-28 ago wenzelm discontinued Sun/Solaris tests;
2010-05-28 ago wenzelm some updates for release;
2010-05-27 ago wenzelm merged
2010-05-27 ago boehmes added function update examples and set examples
2010-05-27 ago boehmes updated SMT certificates
2010-05-27 ago boehmes 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 ago boehmes merged
2010-05-27 ago boehmes renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-27 ago boehmes made script executable
2010-05-27 ago boehmes use Z3's builtin support for div and mod
2010-05-27 ago boehmes moved SMT into the HOL image
2010-05-27 ago wenzelm slightly odd workaround to ignore markup that is typically displaced;
2010-05-27 ago wenzelm 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;
2010-05-27 ago wenzelm 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 ago wenzelm renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 ago wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27 ago wenzelm misc updates for release;
2010-05-27 ago wenzelm constant Rat.normalize needs to be qualified;
2010-05-27 ago wenzelm merged
2010-05-27 ago haftmann merged
2010-05-26 ago haftmann dropped legacy theorem bindings
2010-05-26 ago haftmann dropped legacy theorem bindings
2010-05-26 ago haftmann dropped legacy theorem bindings
2010-05-26 ago haftmann dropped legacy theorem bindings
2010-05-26 ago haftmann dropped legacy theorem bindings
2010-05-26 ago haftmann normalized references to constant "split"
2010-05-26 ago ballarin Revise locale test theory layout.
2010-05-26 ago ballarin Merge mixins of distinct interpretations with same base.
2010-05-27 ago wenzelm indicate prospective properties;
2010-05-27 ago wenzelm clarified auto_update vs. update;
2010-05-27 ago wenzelm more reactive message handling, notably for follow_caret mode;
2010-05-27 ago wenzelm Command.toString: include id for debugging;
2010-05-26 ago wenzelm merged
2010-05-26 ago wenzelm refer to polyml-5.3.0-old for ppc-darwin;
2010-05-26 ago boehmes try logical and theory abstraction before full abstraction (avoids warnings of linarith)
2010-05-26 ago boehmes updated SMT certificates
2010-05-26 ago boehmes hide constants and types introduced by SMT,
2010-05-26 ago haftmann more convenient order of code equations
2010-05-26 ago wenzelm misc updates for release;
2010-05-25 ago wenzelm eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-25 ago wenzelm moved ML files where they are actually used;
2010-05-25 ago wenzelm 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 ago wenzelm eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
2010-05-25 ago wenzelm eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-25 ago wenzelm tuned -- avoid catch-all exception pattern;
2010-05-25 ago wenzelm updated generated files;
2010-05-25 ago wenzelm merged
2010-05-24 ago webertj merged
2010-05-24 ago webertj Typo fixed.
2010-05-24 ago huffman move HOLCF/Sum_Cpo.thy to HOLCF/Library
2010-05-24 ago huffman move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
2010-05-24 ago huffman move unused pattern match syntax stuff into HOLCF/ex
2010-05-24 ago huffman rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
2010-05-24 ago haftmann more lemmas
2010-05-24 ago haftmann induction and case rules
2010-05-24 ago ballarin Store registrations in efficient data structure.