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

mergesort example: recdef->fun, localized

declare "nat o abs" as default measure for int

repaired accidental commit

result for Swing.now;

replaced \overline by \vec;

updated generated files;

tuned;

updated generated files;

removed junk;

improved section "Rule composition"; tuned;

tuned;

improved section on "Hereditary Harrop Formulae";

more on object-level rules; tuned;

updated generated files;

tuned;

more on local theories; tuned;

some text on local theory specifications;

some more Isar macros;

updated genereted files;

minor tuning and typographic fixes;

tuned refs;

removed rudiments of glossary; tuned outline;

removed rudiments of glossary;

removed unused glossary macros;

updated generated files;

observe usual theory naming conventions;

updated generated files;

tuned;