2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-17 wenzelm 2009-07-17 tuned/modernized subst: Same.operation; renamed typ_subst_TVars to subst_type; renamed subst_TVars to subst_term_types; renamed subst_vars to subst_term; removed unused subst_Vars (covered by subst_term);
2009-07-17 wenzelm 2009-07-17 tuned;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-07-17 wenzelm 2009-07-17 major cleanup, simplification, modernization;
2009-07-17 wenzelm 2009-07-17 eq_type: special case for empty environment;
2009-07-17 wenzelm 2009-07-17 compare types directly -- no need to invoke Type.eq_type with empty environment;
2009-07-16 wenzelm 2009-07-16 incr_indexes (from Proofterm);
2009-07-16 wenzelm 2009-07-16 tuned incr_indexes;
2009-07-16 wenzelm 2009-07-16 tuned incr_tvar_same; export tuned version of incr_indexes_same;
2009-07-16 wenzelm 2009-07-16 added same;
2009-07-16 wenzelm 2009-07-16 tuned map_proof_terms_option; eliminated apsome, apsome'; tuned;
2009-07-16 wenzelm 2009-07-16 export incr_tvar_same; tuned;
2009-07-16 wenzelm 2009-07-16 added map_option;
2009-07-16 wenzelm 2009-07-16 use structure Same;
2009-07-16 wenzelm 2009-07-16 use structure Same; tuned;
2009-07-16 wenzelm 2009-07-16 use structure Same; do not open Envir;
2009-07-16 wenzelm 2009-07-16 use structure Same; tuned signature; tuned comments; tuned;
2009-07-16 wenzelm 2009-07-16 added map;
2009-07-16 wenzelm 2009-07-16 use structure Same; more exports; tuned;
2009-07-16 wenzelm 2009-07-16 Support for copy-avoiding functions on pure values, at the cost of readability.
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;