2009-07-16 wenzelm 2009-07-16 removed obsolete/unused legacy_varify;
2009-07-16 wenzelm 2009-07-16 eliminated legacy_varify;
2009-07-15 wenzelm 2009-07-15 merged
2009-07-15 Christian Urban 2009-07-15 simplified proofs
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-15 wenzelm 2009-07-15 eliminated obsolete legacy_varify;
2009-07-15 wenzelm 2009-07-15 tuned comment;
2009-07-15 nipkow 2009-07-15 Made "prime" executable
2009-07-15 nipkow 2009-07-15 More finite set induction rules
2009-07-15 nipkow 2009-07-15 made upt/upto executable on nat/int by simp
2009-07-14 wenzelm 2009-07-14 removed obsolete/unused legacy_unvarify;
2009-07-14 wenzelm 2009-07-14 tuned prepare_patternT: Term.exists_subtype;
2009-07-14 wenzelm 2009-07-14 tuned paramify_vars: Term_Subst.map_atypsT_option;
2009-07-14 haftmann 2009-07-14 merged
2009-07-14 haftmann 2009-07-14 updated to changes in sources; tuned
2009-07-14 haftmann 2009-07-14 updated to changes in sources; tuned
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-14 haftmann 2009-07-14 NEWS and CONTRIBUTORS
2009-07-13 berghofe 2009-07-13 Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
2009-07-12 nipkow 2009-07-12 more gcd/lcm lemmas
2009-07-12 nipkow 2009-07-12 typo
2009-07-12 nipkow 2009-07-12 resolvd conflict
2009-07-12 nipkow 2009-07-12 More about gcd/lcm, and some cleaning up
2009-07-11 haftmann 2009-07-11 added boolean_algebra type class; tuned lattice duals
2009-07-10 krauss 2009-07-10 move Kleene_Algebra to Library
2009-07-10 haftmann 2009-07-10 merged
2009-07-10 haftmann 2009-07-10 tuned locale interface
2009-07-10 haftmann 2009-07-10 tuned
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-07-10 haftmann 2009-07-10 tuned quickcheck generator for bool
2009-07-10 haftmann 2009-07-10 tuned
2009-07-10 wenzelm 2009-07-10 merged
2009-07-10 wenzelm 2009-07-10 merged
2009-07-10 wenzelm 2009-07-10 tuned varify/unvarify: use Term_Subst.map_XXX combinators;
2009-07-10 wenzelm 2009-07-10 added some generic mapping combinators; share private exception SAME locally;
2009-07-09 krauss 2009-07-09 reorganised; many new lemmas thanks to sledgehammer
2009-07-09 krauss 2009-07-09 tuned
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-07-09 wenzelm 2009-07-09 Sorttab in Pure;
2009-07-09 wenzelm 2009-07-09 removed obsolete CVS Ids;
2009-07-09 wenzelm 2009-07-09 removed obsolete CVS Ids;
2009-07-09 wenzelm 2009-07-09 merged
2009-07-09 wenzelm 2009-07-09 recovered some proofs broken in 0314441a53a6;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-07-09 krauss 2009-07-09 move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
2009-07-09 krauss 2009-07-09 drop unused lemmas
2009-07-09 chaieb 2009-07-09 FPS form a metric space, which justifies the infinte sum notation
2009-07-09 chaieb 2009-07-09 merged
2009-07-05 chaieb 2009-07-05 merged
2009-07-04 chaieb 2009-07-04 merged
2009-07-04 chaieb 2009-07-04 merged
2009-07-02 chaieb 2009-07-02 Gettring rid of sorts hyps
2009-07-08 haftmann 2009-07-08 tuned structure Code internally
2009-07-08 nipkow 2009-07-08 merged
2009-07-08 nipkow 2009-07-08 name fixed
2009-07-07 haftmann 2009-07-07 merged
2009-07-07 haftmann 2009-07-07 merged
2009-07-07 haftmann 2009-07-07 tuned interface of structure Code
2009-07-07 haftmann 2009-07-07 more accurate certificates for constant aliasses
2009-07-07 haftmann 2009-07-07 merged