Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
1000
300
100
50
30
+30
+50
+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.
add lemma inj_of_nat
20070612, by huffman
thm antiquotations
20070612, by huffman
Unfortunately needed patch due to incompatibility with SML  oo is infix and hence can not appear on the left handside of patterns
20070612, by chaieb
changed int stuff into integer for SMLNJ compatibility
20070612, by chaieb
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
less
more

(0)
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip