isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Context Data for the new presburger Method
2007-06-11, by chaieb
A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm
2007-06-11, by chaieb
remove references to constant int::nat=>int
2007-06-11, by huffman
simplify int proofs
2007-06-11, by huffman
modify proofs to avoid referring to int::nat=>int
2007-06-11, by huffman
add int_of_nat versions of lemmas about int::nat=>int
2007-06-11, by huffman
add lemma of_nat_power
2007-06-11, by huffman
add int_of_nat versions of lemmas about int::nat=>int
2007-06-11, by huffman
add abbreviation int_of_nat for of_nat::nat=>int;
2007-06-11, by huffman
disabled theory "Reflected_Presburger" for smlnj (temporarily);
2007-06-10, by wenzelm
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
2007-06-10, by wenzelm
*** empty log message ***
2007-06-10, by nipkow
remove dependencies of proofs on constant int::nat=>int, preparing to remove it
2007-06-09, by huffman
eqtype int -- explicitly encourage overloaded equality;
2007-06-09, by wenzelm
simplified type integer;
2007-06-09, by wenzelm
Adapted Proofterm.bicompose_proof to Larry's changes in
2007-06-08, by berghofe
Method "algebra" solves polynomial equations over (semi)rings
2007-06-08, by chaieb
generalize zpower_number_of_{even,odd} lemmas
2007-06-08, by huffman
deleted comments
2007-06-07, by obua
deleted legacy lemmas
2007-06-07, by obua
somebody elses problem fixed
2007-06-07, by nipkow
filter syntax change
2007-06-07, by nipkow
remove redundant lemmas
2007-06-07, by huffman
remove references to preal-specific theorems
2007-06-07, by huffman
define (1::preal); clean up instance declarations
2007-06-07, by huffman
tuned
2007-06-07, by huffman
instance preal :: ordered_cancel_ab_semigroup_add
2007-06-07, by huffman
use new-style class for sq_ord; rename op << to sq_le
2007-06-06, by huffman

less more | (0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle