Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
updated NEWS etc with "solves" criterion and auto_solves
20090211, by kleing
merged
20090211, by nipkow
Moved Order_Relation into Library and moved some of it into Relation.
20090211, by nipkow
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
20090211, by kleing
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
20090211, by kleing
const_name antiquotations
20090210, by huffman
Repaired a proof that did, after all, refer to the theorem nat_induct2.
20090210, by paulson
merged
20090210, by paulson
Strengthened the induction rule nat_induct2.
20090210, by paulson
Deleted the induction rule nat_induct2, which was too weak and not used even once.
20090210, by paulson
merged
20090209, by nipkow
fix to [arith]
20090209, by nipkow
new attribute "arith" for facts supplied to arith.
20090209, by nipkow
Nicer names in FindTheorems.
20090209, by Timothy Bourke
added Determinants to Library
20090209, by chaieb
Traces, Determinant of square matrices and some properties
20090209, by chaieb
added Euclidean_Space and Glbs to Library
20090209, by chaieb
fixed proof  removed unnecessary sorry
20090209, by chaieb
Fixed theorem reference
20090209, by chaieb
(Real) Vectors in Euclidean space, and elementary linear algebra.
20090209, by chaieb
A generic decision procedure for linear rea arithmetic and normed vector spaces
20090209, by chaieb
Permutations, both general and specifically on finite sets.
20090209, by chaieb
Imports Main in order to avoid the typerep problem
20090209, by chaieb
A theory of greatest lower bounds
20090209, by chaieb
Now imports Fact as suggested by Florian in order to avoid the typerep problem
20090209, by chaieb
Added HOL/Library/Finite_Cartesian_Product.thy to Library
20090209, by chaieb
A formalization of finite cartesian product types
20090209, by chaieb
Proof method 'reify' is now reentrant.
20090209, by hoelzl
added noatps
20090208, by nipkow
check for destination directory, do not allocate it gratuitously
20090207, by haftmann
Isar proof
20090207, by haftmann
merged
20090207, by haftmann
code theorems for nth, list_update
20090207, by haftmann
added bulkload
20090207, by haftmann
code theorems for nth, list_update
20090207, by haftmann
added bulkload
20090207, by haftmann
added Decision_Procs.thy
20090207, by haftmann
merged
20090206, by haftmann
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
20090206, by haftmann
authentic syntax for List.nth
20090206, by haftmann
Merged.
20090206, by berghofe
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
20090206, by blanchet
Automated merge with ssh://chaieb@atbroy100.informatik.tumuenchen.de//home/isabellerepository/repos/isabelle
20090206, by chaieb
fixed import
20090206, by chaieb
merged
20090206, by haftmann
more robust failure in error situations
20090206, by haftmann
mandatory prefix for index conversion operations
20090206, by haftmann
added replace operation
20090206, by haftmann
fixed dependencies : Theory Dense_Linear_Order moved to Library
20090206, by chaieb
Theory Dense_Linear_Order moved to Library
20090206, by chaieb
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
20090206, by chaieb
Updated NEWS about approximation
20090205, by hoelzl
merged
20090205, by haftmann
split of already properly working part of Quickcheck infrastructure
20090205, by haftmann
code attribute applied before user attributes
20090205, by haftmann
moved Random.thy to Library
20090205, by haftmann
Add approximation method
20090205, by hoelzl
Added new Float theory and moved old Library/Float.thy to ComputeFloat
20090205, by hoelzl
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
20090205, by hoelzl
Make some Refute functions public so I can use them in Nitpick,
20090204, by blanchet
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip