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
2010-08-09 haftmann 2010-08-09 merged
2010-08-09 haftmann 2010-08-09 separated foundation of `notes`
2010-08-09 haftmann 2010-08-09 more clear separation into local and global facts
2010-08-09 haftmann 2010-08-09 sharpened and tuned educated guess for canonical class morphism
2010-08-09 haftmann 2010-08-09 minimize sorts in certificate instantiation
2010-08-09 blanchet 2010-08-09 prevent ATP thread for staying around for 1 minute if an exception occurred earlier; this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch
2010-08-09 blanchet 2010-08-09 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
2010-08-09 blanchet 2010-08-09 "declare" -> "declaration" (typo)
2010-08-09 blanchet 2010-08-09 replace "setup" with "declaration"
2010-08-09 blanchet 2010-08-09 disable Nitpick on Cygwin while I'm on vacation; I'll look into the timeout once I'm back
2010-08-09 blanchet 2010-08-09 merged
2010-08-09 blanchet 2010-08-09 use "declaration" instead of "setup" to register Nitpick extensions
2010-08-09 blanchet 2010-08-09 remove needless "open"
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-08-09 blanchet 2010-08-09 fiddle some more with "max_new_relevant_facts_per_iter"
2010-08-09 blanchet 2010-08-09 replace recursion with "fold"
2010-08-09 blanchet 2010-08-09 remove debugging output
2010-08-09 blanchet 2010-08-09 remove now needless "Thm.transfer"
2010-08-09 blanchet 2010-08-09 reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF
2010-08-09 blanchet 2010-08-09 merge