2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-19 ballarin 2008-12-19 Add inherited registrations.
2008-12-18 ballarin 2008-12-18 Refactored: evaluate specification text only in locale declarations.
2008-12-17 ballarin 2008-12-17 Transfer theorems in print_locale.
2008-12-17 ballarin 2008-12-17 Attributes not applied in foundational version of fact.
2008-12-16 ballarin 2008-12-16 Transfer morphism with theory closure.
2008-12-16 ballarin 2008-12-16 Finer-grained activation so that facts from earlier elements are available.
2008-12-16 ballarin 2008-12-16 Transfer theorems before activation.
2008-12-16 ballarin 2008-12-16 Use correct mode when parsing elements and conclusion.
2008-12-14 ballarin 2008-12-14 Strict prefixes in locales expressions.
2008-12-12 ballarin 2008-12-12 Propagate theorems to registrations.
2008-12-12 ballarin 2008-12-12 Automated merge with ssh://ballarin@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-12 ballarin 2008-12-12 Equations in interpretation as goals.
2008-12-11 ballarin 2008-12-11 Interpretation in theories: first version with equations.
2008-12-11 ballarin 2008-12-11 Clarified comment.
2008-12-10 ballarin 2008-12-10 Use prefix component of bindings for locale prefixes.
2008-12-10 ballarin 2008-12-10 Missing dependency
2008-12-10 ballarin 2008-12-10 Preserve idents (expression in sublocale).
2008-12-29 wenzelm 2008-12-29 added POSITION_PROPERTIES;
2008-12-29 wenzelm 2008-12-29 tuned;
2008-12-29 wenzelm 2008-12-29 override toString method;
2008-12-29 wenzelm 2008-12-29 Swing utilities.
2008-12-29 wenzelm 2008-12-29 merged
2008-12-29 wenzelm 2008-12-29 optional exception logging; tuned comments;
2008-12-29 haftmann 2008-12-29 merged
2008-12-29 haftmann 2008-12-29 pretty printer for bindings
2008-12-29 haftmann 2008-12-29 adapted HOL source structure to distribution layout
2008-12-29 wenzelm 2008-12-29 tuned;
2008-12-29 wenzelm 2008-12-29 more markup elements;
2008-12-29 wenzelm 2008-12-29 tuned;
2008-12-29 wenzelm 2008-12-29 merged
2008-12-29 wenzelm 2008-12-29 explicit EventBus for results; removed low-level get_result/try_result;
2008-12-29 wenzelm 2008-12-29 added methods "+" and "-"; event: non-synchronized execution of handlers, based on synchronized snapshot;
2008-12-29 wenzelm 2008-12-29 Generic event bus.
2008-12-29 haftmann 2008-12-29 eliminated fun/val confusion
2008-12-28 huffman 2008-12-28 merged
2008-12-28 huffman 2008-12-28 clean up proofs of lemma Maclaurin
2008-12-28 wenzelm 2008-12-28 disabled old jedit plugin;
2008-12-28 wenzelm 2008-12-28 more markup elements;
2008-12-28 wenzelm 2008-12-28 more markup elements;
2008-12-27 krauss 2008-12-27 removed duplicate sum_case used only by function package; moved projections; hide (open)
2008-12-27 krauss 2008-12-27 tuned NEWS; CONTRIBUTORS
2008-12-27 krauss 2008-12-27 renamed LexOrds.thy to Termination.thy; examples for sizechange method
2008-12-27 wenzelm 2008-12-27 tuned;
2008-12-27 wenzelm 2008-12-27 merged
2008-12-27 wenzelm 2008-12-27 refined execute, which replaces exec/exec2;
2008-12-27 wenzelm 2008-12-27 maintain initial process environment; refined execute, which replaces exec/exec2; tuned;
2008-12-27 haftmann 2008-12-27 merged
2008-12-27 haftmann 2008-12-27 tackling simultaneous val/fun bindings
2008-12-27 wenzelm 2008-12-27 proper class IsabelleSystem -- no longer static; tuned;
2008-12-27 wenzelm 2008-12-27 PATH: /opt/local/bin is back again (required for latex etc.);
2008-12-24 huffman 2008-12-24 merged.
2008-12-24 huffman 2008-12-24 clean up lemmas about ln
2008-12-24 huffman 2008-12-24 clean up lemmas about exp
2008-12-24 huffman 2008-12-24 more proofs about differentiable
2008-12-24 huffman 2008-12-24 use less_iff_Suc_add instead of less_add_one
2008-12-24 huffman 2008-12-24 rearranged subsections; cleaned up some proofs
2008-12-24 huffman 2008-12-24 move theorems about limits from Transcendental.thy to Deriv.thy
2008-12-24 huffman 2008-12-24 cleaned up some proofs; removed redundant simp rules
2008-12-23 huffman 2008-12-23 move sin and cos to their own subsection