2010-08-11 wenzelm 2010-08-11 represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
2010-08-11 wenzelm 2010-08-11 Named_Target;
2010-08-11 wenzelm 2010-08-11 modernized specifications; tuned headers;
2010-08-11 wenzelm 2010-08-11 spelling;
2010-08-11 wenzelm 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-08-11 haftmann 2010-08-11 discontinue old implementation of `foundation`
2010-08-11 haftmann 2010-08-11 moved instantiation target formally to class_target.ML
2010-08-11 haftmann 2010-08-11 NEWS
2010-08-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 print fcomp combinator only monadic in connection with other monadic expressions
2010-08-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 moved overloading target formally to overloading.ML
2010-08-11 haftmann 2010-08-11 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
2010-08-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 whitespace tuning
2010-08-11 haftmann 2010-08-11 remove overloading and instantiation from data slot
2010-08-11 wenzelm 2010-08-11 removed obsolete Toplevel.enter_proof_body;
2010-08-11 wenzelm 2010-08-11 standardized pretty printing of consts (e.g. see find_theorems, print_theory);
2010-08-11 wenzelm 2010-08-11 misc tuning and simplification;
2010-08-11 wenzelm 2010-08-11 simplified/unified command setup;
2010-08-11 wenzelm 2010-08-11 removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);
2010-08-11 wenzelm 2010-08-11 prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining; tuned;
2010-08-11 wenzelm 2010-08-11 prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
2010-08-11 wenzelm 2010-08-11 tuned eval_thms (cf. note etc. in proof.ML);
2010-08-11 wenzelm 2010-08-11 use Pretty.enum convenience;
2010-08-11 wenzelm 2010-08-11 tuned whitespace;
2010-08-11 wenzelm 2010-08-11 more precise and more maintainable dependencies;
2010-08-11 wenzelm 2010-08-11 merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;
2010-08-11 haftmann 2010-08-11 * -> prod
2010-08-11 haftmann 2010-08-11 added .ML extension
2010-08-11 haftmann 2010-08-11 avoid old unnamed infix
2010-08-11 haftmann 2010-08-11 avoid inclusion of Natural module in generated code
2010-08-11 haftmann 2010-08-11 explicit ML extension
2010-08-11 haftmann 2010-08-11 merged
2010-08-10 haftmann 2010-08-10 separate initialisation for overloading and instantiation target
2010-08-10 haftmann 2010-08-10 different foundations for different targets; simplified syntax handling of abbreviations
2010-08-11 Christian Urban 2010-08-11 deleted duplicate lemma
2010-08-10 ballarin 2010-08-10 Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
2010-08-10 haftmann 2010-08-10 basic renumbering
2010-08-10 haftmann 2010-08-10 avoiding redundant primes
2010-08-10 haftmann 2010-08-10 separated type from term parameters
2010-08-10 haftmann 2010-08-10 moved extra_tfrees check for mixfix syntax to Generic_Target
2010-08-10 haftmann 2010-08-10 name and argument grouping tuning
2010-08-10 haftmann 2010-08-10 whitespace tuning
2010-08-10 haftmann 2010-08-10 added generic_target.ML
2010-08-10 haftmann 2010-08-10 try to uniformly follow define/note/abbrev/declaration order as close as possible
2010-08-10 haftmann 2010-08-10 split off structure Generic_Target into separate file
2010-08-10 haftmann 2010-08-10 split off generic parts of target implementations into separate structure
2010-08-10 haftmann 2010-08-10 restructured code for `declaration`
2010-08-10 haftmann 2010-08-10 executable relation operations contributed by Tjark Weber
2010-08-09 haftmann 2010-08-09 factored out foundation of `define` into separate function
2010-08-09 haftmann 2010-08-09 combine declaration and definition of foundation constant
2010-08-09 haftmann 2010-08-09 more appropriate outline of `define`
2010-08-09 haftmann 2010-08-09 backlink definition to target `notes`
2010-08-09 haftmann 2010-08-09 merged
2010-08-09 haftmann 2010-08-09 dropped idle local_facts argument; factored out theory_abbrev and locale_abbrev
2010-08-09 haftmann 2010-08-09 more convenient order
2010-08-09 haftmann 2010-08-09 dropped misleading comments