2009-03-30 huffman 2009-03-30 simplify theorem references
2009-03-30 wenzelm 2009-03-30 added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);
2009-03-30 wenzelm 2009-03-30 tuned spacing and formatting;
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 immler 2009-03-30 terminate watching thread
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 huffman 2009-03-30 no longer delay loading of assoc_fold.ML
2009-03-30 wenzelm 2009-03-30 qualified_name_of: observe empty case;
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 huffman 2009-03-30 merged
2009-03-27 huffman 2009-03-27 add more lemmas for signed comparisons
2009-03-30 krauss 2009-03-30 use standard parsers provided by SpecParse
2009-03-30 krauss 2009-03-30 bstring -> binding
2009-03-30 krauss 2009-03-30 code attribute for tailrec-equations, too; tuned
2009-03-30 krauss 2009-03-30 optimistically add code attribute to .simps without further checks
2009-03-30 krauss 2009-03-30 remove "otherwise" feature from function package which was never really documented or used
2009-03-30 wenzelm 2009-03-30 prep_full_context_statement: explicit record of flags; prep_declaration (for add_locale): disallow autofixed frees;
2009-03-30 Timothy Bourke 2009-03-30 Limit the number of results returned by auto_solves.
2009-03-29 wenzelm 2009-03-29 merged
2009-03-29 ballarin 2009-03-29 Merged.
2009-03-29 ballarin 2009-03-29 In interpretation: equations are not propagated through the hierarchy automatically.
2009-03-29 ballarin 2009-03-29 Normalise equation only for morphism, not thm stored in theory.
2009-03-28 ballarin 2009-03-28 Default mode of qualifiers in locale commands.
2009-03-28 ballarin 2009-03-28 Front matter updated.
2009-03-29 wenzelm 2009-03-29 tuned;
2009-03-29 wenzelm 2009-03-29 simplified Element.activate(_i): singleton version;
2009-03-29 wenzelm 2009-03-29 tuned;
2009-03-29 wenzelm 2009-03-29 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;
2009-03-29 wenzelm 2009-03-29 unified binding prefix terminology;
2009-03-29 wenzelm 2009-03-29 simplified roundup activation interface;
2009-03-28 wenzelm 2009-03-28 merged
2009-03-28 haftmann 2009-03-28 merged
2009-03-28 haftmann 2009-03-28 merged
2009-03-28 haftmann 2009-03-28 second attempt for code_deps command
2009-03-28 haftmann 2009-03-28 merged
2009-03-28 haftmann 2009-03-28 corrected projection of required statement names
2009-03-28 haftmann 2009-03-28 corrected check for additional type variables on rhs of code equations
2009-03-28 haftmann 2009-03-28 not yet fruitful tex experiments with bounding boxes
2009-03-28 wenzelm 2009-03-28 simplified Locale.activate operations, using generic context; misc tuning;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 simplified references to facts, eliminated external note_thmss;
2009-03-28 wenzelm 2009-03-28 added map_facts_refs;
2009-03-28 wenzelm 2009-03-28 tuned;
2009-03-28 wenzelm 2009-03-28 replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-28 wenzelm 2009-03-28 replaced add_binds by singleton bind_term;
2009-03-28 wenzelm 2009-03-28 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-28 wenzelm 2009-03-28 minor tuning;
2009-03-28 wenzelm 2009-03-28 merged
2009-03-28 ballarin 2009-03-28 Merged.
2009-03-28 ballarin 2009-03-28 Corrections to locale syntax.
2009-03-27 ballarin 2009-03-27 Update explanation of locale expressions to locale reimplementation.
2009-03-27 ballarin 2009-03-27 Comments updated.
2009-03-27 chaieb 2009-03-27 fixed proof
2009-03-27 chaieb 2009-03-27 merged
2009-03-27 chaieb 2009-03-27 fps made instance of number_ring
2009-03-27 wenzelm 2009-03-27 updated keywords with polyml-experimental;
2009-03-27 wenzelm 2009-03-27 export position_of;
2009-03-27 haftmann 2009-03-27 dropped infix union