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.
more of_rat lemmas
20070612, by huffman
add function of_rat and related lemmas
20070612, by huffman
turned curry (op opr) into curry op opr  because of smlnj
20070612, by chaieb
Deoverloaded operations for int and real.
20070612, by wenzelm
SML basis with type int representing proper integers, not machine words.
20070612, by wenzelm
Tuned proofs : now use 'algebra ad: ...'
20070612, by chaieb
cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor presimplification
20070612, by chaieb
changed val restriction to local due to smlnj
20070612, by chaieb
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
20070612, by chaieb
Added algebra_tac; tuned;
20070612, by chaieb
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
20070612, by chaieb
algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
20070612, by chaieb
nex example
20070611, by nipkow
Conversion for computation on constants now depends on the context
20070611, by chaieb
tuned setup for the fields instantiation for Groebner Bases;
20070611, by chaieb
Added dependency on file Groebner_Basis.thy
20070611, by chaieb
Added instantiation of algebra method to fields
20070611, by chaieb
hid constant "dom"
20070611, by nipkow
Removed from CVS, since obselete in the new Presburger Method;
20070611, by chaieb
Generated reflected QE procedure for Presburger Arithmetic Cooper's Algorithm  see HOL/ex/Reflected_Presburger.thy
20070611, by chaieb
Added more examples
20070611, by chaieb
Now only contains generic conversion for quantifier elimination in HOL
20070611, by chaieb
A new tactic for Presburger;
20070611, by chaieb
tuned
20070611, by chaieb
Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;
20070611, by chaieb
tuned tactic
20070611, by chaieb
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int  To be fixed
20070611, by chaieb
tuned Proof and Document
20070611, by chaieb
tuned Proof
20070611, by chaieb
A new and cleaned up Theory for QE. for Presburger arithmetic
20070611, by chaieb
Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
20070611, by chaieb
explicitely depends on file groebner.ML
20070611, by chaieb
Context Data for the new presburger Method
20070611, by chaieb
A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic  Cooper's Algorithm
20070611, by chaieb
remove references to constant int::nat=>int
20070611, by huffman
simplify int proofs
20070611, by huffman
modify proofs to avoid referring to int::nat=>int
20070611, by huffman
add int_of_nat versions of lemmas about int::nat=>int
20070611, by huffman
add lemma of_nat_power
20070611, by huffman
add int_of_nat versions of lemmas about int::nat=>int
20070611, by huffman
add abbreviation int_of_nat for of_nat::nat=>int;
20070611, by huffman
disabled theory "Reflected_Presburger" for smlnj (temporarily);
20070610, by wenzelm
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
20070610, by wenzelm
*** empty log message ***
20070610, by nipkow
remove dependencies of proofs on constant int::nat=>int, preparing to remove it
20070609, by huffman
eqtype int  explicitly encourage overloaded equality;
20070609, by wenzelm
simplified type integer;
20070609, by wenzelm
Adapted Proofterm.bicompose_proof to Larry's changes in
20070608, by berghofe
Method "algebra" solves polynomial equations over (semi)rings
20070608, by chaieb
generalize zpower_number_of_{even,odd} lemmas
20070608, by huffman
deleted comments
20070607, by obua
deleted legacy lemmas
20070607, by obua
somebody elses problem fixed
20070607, by nipkow
filter syntax change
20070607, by nipkow
remove redundant lemmas
20070607, by huffman
remove references to prealspecific theorems
20070607, by huffman
define (1::preal); clean up instance declarations
20070607, by huffman
tuned
20070607, by huffman
instance preal :: ordered_cancel_ab_semigroup_add
20070607, by huffman
use newstyle class for sq_ord; rename op << to sq_le
20070606, by huffman
less
more

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