Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-10000
-3000
-1000
-300
-100
-50
-28
+28
+50
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
2007-06-11
chaieb
A new tactic for Presburger;
changeset
|
files
2007-06-11
chaieb
tuned
changeset
|
files
2007-06-11
chaieb
Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;
changeset
|
files
2007-06-11
chaieb
tuned tactic
changeset
|
files
2007-06-11
chaieb
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed
changeset
|
files
2007-06-11
chaieb
tuned Proof and Document
changeset
|
files
2007-06-11
chaieb
tuned Proof
changeset
|
files
2007-06-11
chaieb
A new and cleaned up Theory for QE. for Presburger arithmetic
changeset
|
files
2007-06-11
chaieb
Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
changeset
|
files
2007-06-11
chaieb
explicitely depends on file groebner.ML
changeset
|
files
2007-06-11
chaieb
Context Data for the new presburger Method
changeset
|
files
2007-06-11
chaieb
A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm
changeset
|
files
2007-06-11
huffman
remove references to constant int::nat=>int
changeset
|
files
2007-06-11
huffman
simplify int proofs
changeset
|
files
2007-06-11
huffman
modify proofs to avoid referring to int::nat=>int
changeset
|
files
2007-06-11
huffman
add int_of_nat versions of lemmas about int::nat=>int
changeset
|
files
2007-06-11
huffman
add lemma of_nat_power
changeset
|
files
2007-06-10
huffman
add int_of_nat versions of lemmas about int::nat=>int
changeset
|
files
2007-06-10
huffman
add abbreviation int_of_nat for of_nat::nat=>int;
changeset
|
files
2007-06-10
wenzelm
disabled theory "Reflected_Presburger" for smlnj (temporarily);
changeset
|
files
2007-06-10
wenzelm
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
changeset
|
files
2007-06-10
nipkow
*** empty log message ***
changeset
|
files
2007-06-09
huffman
remove dependencies of proofs on constant int::nat=>int, preparing to remove it
changeset
|
files
2007-06-08
wenzelm
eqtype int -- explicitly encourage overloaded equality;
changeset
|
files
2007-06-08
wenzelm
simplified type integer;
changeset
|
files
2007-06-08
berghofe
Adapted Proofterm.bicompose_proof to Larry's changes in
changeset
|
files
2007-06-08
chaieb
Method "algebra" solves polynomial equations over (semi)rings
changeset
|
files
2007-06-08
huffman
generalize zpower_number_of_{even,odd} lemmas
changeset
|
files
(0)
-10000
-3000
-1000
-300
-100
-50
-28
+28
+50
+100
+300
+1000
+3000
+10000
+30000
tip