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 -32 +32 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Method.Basic: include position;
2007-06-13, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-13, by wenzelm
Basic text: include position;
2007-06-13, by wenzelm
thm antiquotations
2007-06-12, by huffman
add lemma inj_of_nat
2007-06-12, by huffman
thm antiquotations
2007-06-12, by huffman
Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns
2007-06-12, by chaieb
changed int stuff into integer for SMLNJ compatibility
2007-06-12, by chaieb
more of_rat lemmas
2007-06-12, by huffman
add function of_rat and related lemmas
2007-06-12, by huffman
turned curry (op opr) into curry op opr --- because of smlnj
2007-06-12, by chaieb
De-overloaded operations for int and real.
2007-06-12, by wenzelm
SML basis with type int representing proper integers, not machine words.
2007-06-12, by wenzelm
Tuned proofs : now use 'algebra ad: ...'
2007-06-12, by chaieb
cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification
2007-06-12, by chaieb
changed val restriction to local due to smlnj
2007-06-12, 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;
2007-06-12, by chaieb
Added algebra_tac; tuned;
2007-06-12, by chaieb
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
2007-06-12, 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
2007-06-12, by chaieb
nex example
2007-06-11, by nipkow
Conversion for computation on constants now depends on the context
2007-06-11, by chaieb
tuned setup for the fields instantiation for Groebner Bases;
2007-06-11, by chaieb
Added dependency on file Groebner_Basis.thy
2007-06-11, by chaieb
Added instantiation of algebra method to fields
2007-06-11, by chaieb
hid constant "dom"
2007-06-11, by nipkow
Removed from CVS, since obselete in the new Presburger Method;
2007-06-11, by chaieb
Generated reflected QE procedure for Presburger Arithmetic-- Cooper's Algorithm -- see HOL/ex/Reflected_Presburger.thy
2007-06-11, by chaieb
Added more examples
2007-06-11, by chaieb
Now only contains generic conversion for quantifier elimination in HOL
2007-06-11, by chaieb
A new tactic for Presburger;
2007-06-11, by chaieb
tuned
2007-06-11, by chaieb

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

isabelle