2009-11-13 wenzelm 2009-11-13 inductive: eliminated obsolete kind;
2009-11-13 paulson 2009-11-13 merged
2009-11-13 paulson 2009-11-13 A little rationalisation
2009-11-13 wenzelm 2009-11-13 eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-13 boehmes 2009-11-13 merged
2009-11-13 boehmes 2009-11-13 removed unused code and unused arguments, tuned
2009-11-13 boehmes 2009-11-13 adapted proofs due to changes in HOL-Boogie
2009-11-13 boehmes 2009-11-13 parallel solving of Boogie splinters
2009-11-13 boehmes 2009-11-13 corrected translation of integer operators, keep argument order for n-ary symbols (conjunction, disjunction), removed unused code
2009-11-13 boehmes 2009-11-13 extended theory simpset to simplify non-linear problems
2009-11-13 wenzelm 2009-11-13 more "anti_sym" -> "antisym" (cf. a4179bf442d1);
2009-11-13 nipkow 2009-11-13 merged
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
2009-11-13 krauss 2009-11-13 a few lemmas for point-free reasoning about transitive closure
2009-11-13 paulson 2009-11-13 merged
2009-11-13 paulson 2009-11-13 A number of theorems contributed by Jeremy Avigad
2009-11-13 bulwahn 2009-11-13 merged
2009-11-12 bulwahn 2009-11-12 merged
2009-11-12 bulwahn 2009-11-12 adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
2009-11-12 bulwahn 2009-11-12 removed annoying tracing message
2009-11-12 bulwahn 2009-11-12 added a tabled implementation of the reflexive transitive closure
2009-11-12 huffman 2009-11-12 merged
2009-11-12 huffman 2009-11-12 merged
2009-11-12 huffman 2009-11-12 improved ML interface to pcpodef
2009-11-11 huffman 2009-11-11 use Drule.standard (following typedef package), add pcpodef tactic interface
2009-11-12 wenzelm 2009-11-12 eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-12 wenzelm 2009-11-12 unused_thms: ignore kind -- already observes "concealed" flag;
2009-11-12 wenzelm 2009-11-12 all_valid_thms: more sophisticated check against global + local name space;
2009-11-12 hoelzl 2009-11-12 Remove map_compose, replaced by map_map
2009-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-11-12 hoelzl 2009-11-12 Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
2009-11-12 haftmann 2009-11-12 merged
2009-11-12 haftmann 2009-11-12 accomplish mutual recursion between fun and inst
2009-11-12 haftmann 2009-11-12 moved lemma map_of_zip_map to Map.thy
2009-11-12 haftmann 2009-11-12 merged
2009-11-12 haftmann 2009-11-12 explicit code lemmas produce nices code
2009-11-12 haftmann 2009-11-12 repaired broken code_const for term_of [String.literal]
2009-11-12 blanchet 2009-11-12 fixed soundness bug in Nitpick related to sets
2009-11-12 bulwahn 2009-11-12 removed unnecessary oracle in the predicate compiler
2009-11-12 bulwahn 2009-11-12 improving code quality thanks to Florian's code review
2009-11-12 bulwahn 2009-11-12 renaming code_pred_intros to code_pred_intro * * * adopted alternative definitions for the predicate compiler to new attribute name
2009-11-12 bulwahn 2009-11-12 announcing the predicate compiler in NEWS and CONTRIBUTORS
2009-11-12 bulwahn 2009-11-12 new names for predicate functions in the predicate compiler * * * adopting examples of the predicate compiler
2009-11-12 bulwahn 2009-11-12 removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming
2009-11-12 bulwahn 2009-11-12 added another example to the predicate compiler * * * tuning examples
2009-11-12 bulwahn 2009-11-12 changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
2009-11-12 bulwahn 2009-11-12 removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
2009-11-12 bulwahn 2009-11-12 adopted predicate compiler examples to new syntax for modes
2009-11-12 bulwahn 2009-11-12 added interface of user proposals for names of generated constants
2009-11-12 bulwahn 2009-11-12 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
2009-11-12 bulwahn 2009-11-12 adding more tests for the values command; adding some forbidden constants to inductify * * * added further testcase for values command
2009-11-11 ballarin 2009-11-11 Enables tests for locale functionality that is now available.
2009-11-11 wenzelm 2009-11-11 merged
2009-11-11 wenzelm 2009-11-11 uniform use of simultabeous use_thys;
2009-11-11 haftmann 2009-11-11 merged
2009-11-11 haftmann 2009-11-11 explicit invocation of code generation
2009-11-11 haftmann 2009-11-11 adding code equations for constructors
2009-11-11 haftmann 2009-11-11 tuned
2009-11-11 boehmes 2009-11-11 changed URL of SMT server, added Z3 rewrite lemma