add lemma surj_from_nat

fix document generation

merged

fix document generation

section -> subsection

add instance for cancel_comm_monoid_add

add class cancel_comm_monoid_add

more finiteness changes

merged

finiteness lemmas

merged

unset execute bit

Tuned datatype antiquotation.

made SMLNJ happy

typo

find_consts: display the search criteria. (by Timothy Bourke)

find_consts: documentation. (by Timothy Bourke)

FindTheorems solves: update documentation (by Timothy Bourke)

fixed codegen tool

merged

fixed codegen tool

merged

Moved Nat_Int_Bij into Library

removed Reflection session

add lemma add_nonneg_eq_0_iff

add lemmas about sgn

added ML file for the find_consts command

added find_consts to NEWS and CONTRIBUTORS

New command find_consts searching for constants by type (by Timothy Bourke).

fix document generation

move countability proof from Rational to Countable; add instance rat :: countable

Moved FTA into Lib and cleaned it up a little.

ordered_idom instance for polynomials

Export tactic interface for sizechange method

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