2009-02-13 kleing 2009-02-13 added find_consts to NEWS and CONTRIBUTORS
2009-02-13 kleing 2009-02-13 New command find_consts searching for constants by type (by Timothy Bourke).
2009-02-12 huffman 2009-02-12 fix document generation
2009-02-12 huffman 2009-02-12 move countability proof from Rational to Countable; add instance rat :: countable
2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little.
2009-02-11 huffman 2009-02-11 ordered_idom instance for polynomials
2009-02-11 krauss 2009-02-11 Export tactic interface for sizechange method
2009-02-11 haftmann 2009-02-11 merged
2009-02-11 haftmann 2009-02-11 liberal inst_meet
2009-02-11 haftmann 2009-02-11 display code theorems with HOL equality
2009-02-11 blanchet 2009-02-11 merged
2009-02-10 blanchet 2009-02-10 Added serial_string to SAT solver input and output files, to prevent multithreading chaos. Bug reported by Tobias.
2009-02-10 blanchet 2009-02-10 Added nitpick_const_simp attribute to recdef and record packages.
2009-02-10 blanchet 2009-02-10 Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.
2009-02-10 blanchet 2009-02-10 Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.
2009-02-09 blanchet 2009-02-09 Reintroduced nitpick_ind_intro attribute. It looks like I need it nonetheless.
2009-02-09 blanchet 2009-02-09 merged
2009-02-09 blanchet 2009-02-09 Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.
2009-02-06 blanchet 2009-02-06 merged
2009-02-06 blanchet 2009-02-06 Merged.
2009-02-06 blanchet 2009-02-06 Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.
2009-02-11 kleing 2009-02-11 fixed typo
2009-02-11 kleing 2009-02-11 updated NEWS etc with "solves" criterion and auto_solves
2009-02-11 nipkow 2009-02-11 merged
2009-02-11 nipkow 2009-02-11 Moved Order_Relation into Library and moved some of it into Relation.
2009-02-11 kleing 2009-02-11 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
2009-02-11 kleing 2009-02-11 FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-02-10 huffman 2009-02-10 const_name antiquotations
2009-02-10 paulson 2009-02-10 Repaired a proof that did, after all, refer to the theorem nat_induct2.
2009-02-10 paulson 2009-02-10 merged
2009-02-10 paulson 2009-02-10 Strengthened the induction rule nat_induct2.
2009-02-10 paulson 2009-02-10 Deleted the induction rule nat_induct2, which was too weak and not used even once.
2009-02-09 nipkow 2009-02-09 merged
2009-02-09 nipkow 2009-02-09 fix to [arith]
2009-02-09 nipkow 2009-02-09 new attribute "arith" for facts supplied to arith.
2009-02-09 Timothy Bourke 2009-02-09 Nicer names in FindTheorems. * Patch NameSpace.get_accesses, contributed by Timothy Bourke: NameSpace.get_accesses has been patched to fix the following bug: theory OverHOL imports Main begin lemma conjI: "a & b --> b" by blast ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of; val x1 = NameSpace.get_accesses ns "HOL.conjI"; val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *} end where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"], but x1 should be just ["HOL.conjI"]. NameSpace.get_accesses is only used within the NameSpace structure itself. The two uses have been modified to retain their original behaviour. Note that NameSpace.valid_accesses gives different results: get_accesses ns "HOL.eq_class.eq" gives ["eq", "eq_class.eq", "HOL.eq_class.eq"] but, valid_accesses ns "HOL.eq_class.eq" gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"] * Patch FindTheorems: Prefer names that are shorter to type in the current context. * Re-export space_of.
2009-02-09 chaieb 2009-02-09 added Determinants to Library
2009-02-09 chaieb 2009-02-09 Traces, Determinant of square matrices and some properties
2009-02-09 chaieb 2009-02-09 added Euclidean_Space and Glbs to Library
2009-02-09 chaieb 2009-02-09 fixed proof -- removed unnecessary sorry
2009-02-09 chaieb 2009-02-09 Fixed theorem reference
2009-02-09 chaieb 2009-02-09 (Real) Vectors in Euclidean space, and elementary linear algebra.
2009-02-09 chaieb 2009-02-09 A generic decision procedure for linear rea arithmetic and normed vector spaces
2009-02-09 chaieb 2009-02-09 Permutations, both general and specifically on finite sets.
2009-02-09 chaieb 2009-02-09 Imports Main in order to avoid the typerep problem
2009-02-09 chaieb 2009-02-09 A theory of greatest lower bounds
2009-02-09 chaieb 2009-02-09 Now imports Fact as suggested by Florian in order to avoid the typerep problem
2009-02-09 chaieb 2009-02-09 Added HOL/Library/Finite_Cartesian_Product.thy to Library
2009-02-09 chaieb 2009-02-09 A formalization of finite cartesian product types
2009-02-09 hoelzl 2009-02-09 Proof method 'reify' is now reentrant.
2009-02-08 nipkow 2009-02-08 added noatps
2009-02-07 haftmann 2009-02-07 check for destination directory, do not allocate it gratuitously
2009-02-07 haftmann 2009-02-07 Isar proof
2009-02-07 haftmann 2009-02-07 merged
2009-02-07 haftmann 2009-02-07 code theorems for nth, list_update
2009-02-07 haftmann 2009-02-07 added bulkload
2009-02-07 haftmann 2009-02-07 code theorems for nth, list_update
2009-02-07 haftmann 2009-02-07 added bulkload
2009-02-07 haftmann 2009-02-07 added Decision_Procs.thy
2009-02-06 haftmann 2009-02-06 merged