2010-03-21 wenzelm 2010-03-21 eliminated old constdefs;
2010-03-21 haftmann 2010-03-21 corrected setup for of_list
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-20 Christian Urban 2010-03-20 added lemma infinite_Un
2010-03-19 Cezary Kaliszyk 2010-03-19 Check that argument is not a 'Bound' before calling fastype_of.
2010-03-19 wenzelm 2010-03-19 typedef etc.: no constraints;
2010-03-19 wenzelm 2010-03-19 allow sort constraints in HOL/typedef;
2010-03-19 wenzelm 2010-03-19 allow sort constraints in HOL/typedef and related HOLCF variants;
2010-03-19 wenzelm 2010-03-19 OuterParse.type_args_constrained;
2010-03-19 wenzelm 2010-03-19 support type arguments with sort constraints;
2010-03-18 wenzelm 2010-03-18 typedecl: no sort constraints; prefer Name.invents over old-style Name.variant_list;
2010-03-18 wenzelm 2010-03-18 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
2010-03-18 wenzelm 2010-03-18 typedecl: no sort constraints;
2010-03-18 wenzelm 2010-03-18 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types); allow sort constraints; misc tuning and clarification;
2010-03-16 hoelzl 2010-03-16 Added product measure space
2010-03-18 blanchet 2010-03-18 added type constraints to make SML/NJ happy
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 fix Mirabelle after renaming Sledgehammer structures
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 blanchet 2010-03-17 renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-17 blanchet 2010-03-17 renamed Sledgehammer structures
2010-03-17 blanchet 2010-03-17 move Sledgehammer files in a directory of their own
2010-03-18 haftmann 2010-03-18 merged
2010-03-18 haftmann 2010-03-18 dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18 haftmann 2010-03-18 lemma swap_inj_on, swap_product
2010-03-18 haftmann 2010-03-18 meaningful transfer certificate
2010-03-18 haftmann 2010-03-18 dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule
2010-03-18 haftmann 2010-03-18 updated certificate
2010-03-18 haftmann 2010-03-18 dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18 haftmann 2010-03-18 added locales folding_one_(idem); various streamlining and tuning
2010-03-18 haftmann 2010-03-18 generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-17 boehmes 2010-03-17 tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-17 blanchet 2010-03-17 added one-entry cache around Kodkod invocation
2010-03-17 blanchet 2010-03-17 merged
2010-03-17 blanchet 2010-03-17 solve error in "Nitpick_Mono" + short path when no finite functions are inferred
2010-03-17 blanchet 2010-03-17 minor additions to Nitpick docs
2010-03-17 huffman 2010-03-17 NEWS: Nat_Bijection library
2010-03-17 blanchet 2010-03-17 document "nitpick_choice_spec" attribute
2010-03-17 blanchet 2010-03-17 fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-16 Christian Urban 2010-03-16 rollback of local typedef until problem with type-variables can be sorted out; fixed header
2010-03-16 haftmann 2010-03-16 adjusted to changes in Finite_Set
2010-03-15 wenzelm 2010-03-15 merged
2010-03-15 nipkow 2010-03-15 merged
2010-03-15 nipkow 2010-03-15 tuned inductions
2010-03-15 wenzelm 2010-03-15 tuned;
2010-03-15 wenzelm 2010-03-15 moved old Sign.intern_term to the place where it is still used;
2010-03-15 wenzelm 2010-03-15 preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
2010-03-15 wenzelm 2010-03-15 replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-15 haftmann 2010-03-15 merged
2010-03-15 haftmann 2010-03-15 corrected disastrous syntax declarations
2010-03-15 haftmann 2010-03-15 added stmaryrd for isasymSqinter
2010-03-14 huffman 2010-03-14 use headers consistently
2010-03-14 huffman 2010-03-14 no_document for theory Countable
2010-03-14 huffman 2010-03-14 old domain package also defines map functions
2010-03-14 huffman 2010-03-14 separate map-related code into new function define_map_functions
2010-03-14 Christian Urban 2010-03-14 removed Local_Theory.theory_result by using local Typedef.add_typedef
2010-03-14 wenzelm 2010-03-14 tuned comment;
2010-03-14 wenzelm 2010-03-14 observe standard header format;