2010-03-22 boehmes 2010-03-22 provide a hook to safely manipulate verification conditions
2010-03-22 boehmes 2010-03-22 replaced old-style Drule.add_axiom by Specification.axiomatization
2010-03-22 boehmes 2010-03-22 removed e-mail address from error message
2010-03-22 haftmann 2010-03-22 merged
2010-03-21 haftmann 2010-03-21 tuned whitespace
2010-03-21 haftmann 2010-03-21 handle hidden polymorphism in class target (without class target syntax, though)
2010-03-22 wenzelm 2010-03-22 replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-21 wenzelm 2010-03-21 add_axiom: axiomatize "unconstrained" version, with explicit of_class premises; more uniform add_axiom/add_def;
2010-03-21 wenzelm 2010-03-21 Logic.mk_of_sort convenience;
2010-03-21 wenzelm 2010-03-21 more explicit invented name;
2010-03-21 wenzelm 2010-03-21 minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-21 wenzelm 2010-03-21 do not open ML structures;
2010-03-21 wenzelm 2010-03-21 modernized overloaded definitions;
2010-03-21 wenzelm 2010-03-21 standard headers;
2010-03-21 wenzelm 2010-03-21 slightly more uniform definitions -- eliminated old-style meta-equality;
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