2009-04-29 huffman 2009-04-29 reimplement reorientation simproc using theory data
2009-04-29 huffman 2009-04-29 use opaque ascription for all HOLCF code
2009-04-29 nipkow 2009-04-29 added listsum lemmas
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-28 haftmann 2009-04-28 merged
2009-04-28 haftmann 2009-04-28 power constraint needed, though
2009-04-28 haftmann 2009-04-28 stripped lemma duplicatesrc/HOL/Word/Num_Lemmas.thy
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-04-28 haftmann 2009-04-28 lemma sum_nonneg_eq_zero_iff
2009-04-28 haftmann 2009-04-28 reorganization of power lemmas
2009-04-28 haftmann 2009-04-28 collected square lemmas in Nat_Numeral
2009-04-28 haftmann 2009-04-28 Symbol.name_of and Name.desymbolize
2009-04-28 haftmann 2009-04-28 prevent potential failure
2009-04-28 haftmann 2009-04-28 ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms
2009-04-28 haftmann 2009-04-28 local syntax for Ints; ephermal re-globalization
2009-04-28 haftmann 2009-04-28 dropped reference to class recpower and lemma duplicate
2009-04-27 huffman 2009-04-27 add proper support for bottom-patterns in fixrec package
2009-04-27 huffman 2009-04-27 merged
2009-04-22 huffman 2009-04-22 add module signature to domain_library.ML
2009-04-22 huffman 2009-04-22 add module signature for domain_theorems.ML
2009-04-22 huffman 2009-04-22 declare take_rews as simp rules
2009-04-27 haftmann 2009-04-27 explicit is better than implicit
2009-04-27 haftmann 2009-04-27 whitespace tuning
2009-04-27 haftmann 2009-04-27 cleaned up theory power further
2009-04-27 haftmann 2009-04-27 merged
2009-04-26 haftmann 2009-04-26 merged
2009-04-26 haftmann 2009-04-26 merged
2009-04-26 haftmann 2009-04-26 fixed document generation
2009-04-26 haftmann 2009-04-26 cleaned up Power theory
2009-04-26 chaieb 2009-04-26 merged
2009-04-26 chaieb 2009-04-26 merged
2009-04-24 chaieb 2009-04-24 merged
2009-04-24 chaieb 2009-04-24 more general statements
2009-04-27 Christian Urban 2009-04-27 tuned
2009-04-26 Christian Urban 2009-04-26 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
2009-04-26 haftmann 2009-04-26 reverted slip in theory imports
2009-04-26 haftmann 2009-04-26 adjusted to changes in power syntax
2009-04-26 Christian Urban 2009-04-26 merged
2009-04-26 Christian Urban 2009-04-26 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
2009-04-25 wenzelm 2009-04-25 append prefs at end;
2009-04-25 wenzelm 2009-04-25 merged
2009-04-25 Christian Urban 2009-04-25 adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
2009-04-25 wenzelm 2009-04-25 use predefined preferences categories;
2009-04-25 wenzelm 2009-04-25 removed obsolete artifacts;
2009-04-25 wenzelm 2009-04-25 misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place;
2009-04-25 wenzelm 2009-04-25 renamed contrib/SystemOnTPTP/remote to lib/script/SystemOnTPTP, thus leaving contrib empty within the official distribution;
2009-04-25 wenzelm 2009-04-25 post Isabelle2009 version;
2009-04-25 haftmann 2009-04-25 adjusted to change in code_wellsorted.ML
2009-04-24 haftmann 2009-04-24 merged
2009-04-24 haftmann 2009-04-24 some jokes are just too bad to appear in a theory file
2009-04-24 haftmann 2009-04-24 removed confusion around funpow
2009-04-24 haftmann 2009-04-24 observe distinction between Pure/Tools and Tools more closely
2009-04-24 haftmann 2009-04-24 some experiements towards user interface for predicate compiler
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-24 haftmann 2009-04-24 generic postprocessing scheme for term evaluations
2009-04-24 haftmann 2009-04-24 added helpless comment
2009-04-23 haftmann 2009-04-23 adaptions due to rearrangment of power operation
2009-04-23 haftmann 2009-04-23 stripped $Id$
2009-04-23 haftmann 2009-04-23 avoid local [code]
2009-04-22 haftmann 2009-04-22 dropped duplication