merged

liberal inst_meet

display code theorems with HOL equality

merged

Added serial_string to SAT solver input and output files, to prevent multithreading chaos. Bug reported by Tobias.

Added nitpick_const_simp attribute to recdef and record packages.

Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.

Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.

Reintroduced nitpick_ind_intro attribute. It looks like I need it nonetheless.

merged

Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.

merged

Merged.

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.

fixed typo

updated NEWS etc with "solves" criterion and auto_solves

merged

Moved Order_Relation into Library and moved some of it into Relation.

Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke

FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke

const_name antiquotations

Repaired a proof that did, after all, refer to the theorem nat_induct2.

merged

Strengthened the induction rule nat_induct2.

Deleted the induction rule nat_induct2, which was too weak and not used even once.

merged

fix to [arith]

new attribute "arith" for facts supplied to arith.

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.

added Determinants to Library

Traces, Determinant of square matrices and some properties

added Euclidean_Space and Glbs to Library

fixed proof -- removed unnecessary sorry

Fixed theorem reference

(Real) Vectors in Euclidean space, and elementary linear algebra.

A generic decision procedure for linear rea arithmetic and normed vector spaces

Permutations, both general and specifically on finite sets.

Imports Main in order to avoid the typerep problem

A theory of greatest lower bounds

Now imports Fact as suggested by Florian in order to avoid the typerep problem

Added HOL/Library/Finite_Cartesian_Product.thy to Library

A formalization of finite cartesian product types

Proof method 'reify' is now reentrant.

added noatps

check for destination directory, do not allocate it gratuitously

Isar proof

merged

code theorems for nth, list_update

added bulkload

code theorems for nth, list_update

added bulkload

added Decision_Procs.thy

merged

session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there

authentic syntax for List.nth

Merged.

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.

Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

fixed import

merged

more robust failure in error situations

mandatory prefix for index conversion operations

added replace operation

fixed dependencies : Theory Dense_Linear_Order moved to Library

Theory Dense_Linear_Order moved to Library

fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library

Updated NEWS about approximation

merged

split of already properly working part of Quickcheck infrastructure

code attribute applied before user attributes

moved Random.thy to Library

Add approximation method

Added new Float theory and moved old Library/Float.thy to ComputeFloat

Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series

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.

merged

Now catch ERROR exception thrown by find and friends

dropped Id

proper datatype abstraction example

handling type classes without parameters

adjusted theory name

merged

added stub about datatype abstraction

changed name space policy for Haskell includes

merged Big0

added ROOT.ML for Reflection session

merged

established session HOL-Reflection

established session HOL-Reflection

regenerated presburger code

merged Big0

merge

changed default timeout

merged

dropped global Nil/Append interpretation

small fixes; removed Id