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.
merged
20090209, by blanchet
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
20090209, by blanchet
merged
20090206, by blanchet
Merged.
20090206, by blanchet
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
20090206, by blanchet
fixed typo
20090211, by kleing
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
less
more

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