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
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
2009-02-06 haftmann 2009-02-06 authentic syntax for List.nth
2009-02-06 berghofe 2009-02-06 Merged.
2009-02-06 blanchet 2009-02-06 Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.
2009-02-06 chaieb 2009-02-06 Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-02-06 chaieb 2009-02-06 fixed import
2009-02-06 haftmann 2009-02-06 merged
2009-02-06 haftmann 2009-02-06 more robust failure in error situations
2009-02-06 haftmann 2009-02-06 mandatory prefix for index conversion operations
2009-02-06 haftmann 2009-02-06 added replace operation
2009-02-06 chaieb 2009-02-06 fixed dependencies : Theory Dense_Linear_Order moved to Library
2009-02-06 chaieb 2009-02-06 Theory Dense_Linear_Order moved to Library
2009-02-06 chaieb 2009-02-06 fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
2009-02-05 hoelzl 2009-02-05 Updated NEWS about approximation
2009-02-05 haftmann 2009-02-05 merged
2009-02-05 haftmann 2009-02-05 split of already properly working part of Quickcheck infrastructure
2009-02-05 haftmann 2009-02-05 code attribute applied before user attributes
2009-02-05 haftmann 2009-02-05 moved Random.thy to Library
2009-02-05 hoelzl 2009-02-05 Add approximation method
2009-02-05 hoelzl 2009-02-05 Added new Float theory and moved old Library/Float.thy to ComputeFloat
2009-02-05 hoelzl 2009-02-05 Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2009-02-04 blanchet 2009-02-04 Make some Refute functions public so I can use them in Nitpick, use @{const_name} antiquotation whenever possible (some, like Lfp.lfp had been renamed since Tjark wrote Refute), and removed some "set"-related code that is no longer relevant in Isabelle2008. There's still some "set" code that needs to be ported; see TODO in the file.
2009-02-04 chaieb 2009-02-04 merged