summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

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.