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.
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
take out Class.thy again, because it does not yet compile cleanly
20070606, by urbanc
add axclass semiring_char_0 for types where of_nat is injective
20070606, by huffman
changed filter syntax from : to <
20070606, by nipkow
hide filter
20070606, by nipkow
tuned list comprehension, changed filter syntax from : to <
20070606, by nipkow
clean up proofs of exp_zero, sin_zero, cos_zero
20070606, by huffman
generalize class constraints on some lemmas
20070606, by huffman
generalize of_nat and related constants to class semiring_1
20070606, by huffman
declare complex_diff as simp rule
20070606, by huffman
New Reflected Presburger added to HOL/ex
20070606, by chaieb
Groebner Basis Examples.
20070605, by wenzelm
print_antiquotations: sort_strings;
20070605, by wenzelm
tuned document;
20070605, by wenzelm
tuned source deps;
20070605, by wenzelm
simplified/renamed add_numerals;
20070605, by wenzelm
renamed ex/Eval_Examples.thy;
20070605, by wenzelm
added ex/Groebner_Examples.thy;
20070605, by wenzelm
tuned document;
20070605, by wenzelm
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
20070605, by chaieb
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
20070605, by chaieb
tuned boostrap
20070605, by haftmann
eliminated Code_Generator.thy
20070605, by haftmann
tuned integers
20070605, by haftmann
tuned;
20070605, by wenzelm
fixed type int vs. integer;
20070605, by wenzelm
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
20070605, by wenzelm
less
more

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