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

instance preal :: ordered_cancel_ab_semigroup_add
2007-06-07, by huffman
use new-style class for sq_ord; rename op << to sq_le
2007-06-06, by huffman
take out Class.thy again, because it does not yet compile cleanly
2007-06-06, by urbanc
add axclass semiring_char_0 for types where of_nat is injective
2007-06-06, by huffman
changed filter syntax from : to <-
2007-06-06, by nipkow
hide filter
2007-06-06, by nipkow
tuned list comprehension, changed filter syntax from : to <-
2007-06-06, by nipkow
clean up proofs of exp_zero, sin_zero, cos_zero
2007-06-06, by huffman
generalize class constraints on some lemmas
2007-06-06, by huffman
generalize of_nat and related constants to class semiring_1
2007-06-06, by huffman
declare complex_diff as simp rule
2007-06-06, by huffman
New Reflected Presburger added to HOL/ex
2007-06-06, by chaieb
Groebner Basis Examples.
2007-06-05, by wenzelm
print_antiquotations: sort_strings;
2007-06-05, by wenzelm
tuned document;
2007-06-05, by wenzelm
tuned source deps;
2007-06-05, by wenzelm
simplified/renamed add_numerals;
2007-06-05, by wenzelm
renamed ex/Eval_Examples.thy;
2007-06-05, by wenzelm
added ex/Groebner_Examples.thy;
2007-06-05, by wenzelm
tuned document;
2007-06-05, by wenzelm
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
2007-06-05, by chaieb
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
2007-06-05, by chaieb
tuned boostrap
2007-06-05, by haftmann
eliminated Code_Generator.thy
2007-06-05, by haftmann
tuned integers
2007-06-05, by haftmann
tuned;
2007-06-05, by wenzelm
fixed type int vs. integer;
2007-06-05, by wenzelm
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
2007-06-05, by wenzelm
add new lemmas
2007-06-05, by huffman
Polynomials now only depend on Deriv; Definition of degree changed
2007-06-05, by chaieb
lemma lemma_DERIV_subst moved to Deriv.thy
2007-06-05, by chaieb
tuned proofs;
2007-06-05, by wenzelm
tuned comments;
2007-06-05, by wenzelm
Semiring normalization and Groebner Bases.
2007-06-05, by wenzelm
moved generic algebra modules
2007-06-05, by haftmann
updated documentation
2007-06-05, by haftmann
fixed broken execption handling
2007-06-05, by haftmann
simplified notion of "operational classes"
2007-06-05, by haftmann
merged Code_Generator.thy into HOL.thy
2007-06-05, by haftmann
added a function partition and a few lemmas
2007-06-05, by chaieb
added a few theorems about foldl and set
2007-06-05, by chaieb
added lcm, ilcm (lcm for integers) and some lemmas about them;
2007-06-05, by chaieb
included Class.thy in the compiling process for Nominal/Examples
2007-06-05, by urbanc
remove simp attribute from lemma_STAR theorems
2007-06-05, by huffman
add lemma exp_of_real
2007-06-05, by huffman
tuned list comprehension
2007-06-04, by nipkow
tuned;
2007-06-04, by wenzelm
added is_atomic;
2007-06-04, by wenzelm
added assume_rule_tac;
2007-06-04, by wenzelm
reverted appnd to append
2007-06-04, by haftmann
authentic syntax for List.append
2007-06-04, by haftmann
tuned comments
2007-06-04, by haftmann
added a few comments to the proofs
2007-06-04, by urbanc
removed fixmes
2007-06-04, by chaieb
opaque-constraint removed
2007-06-04, by chaieb
tuned;
2007-06-04, by chaieb
monomorphic equality: let ML work out the details;
2007-06-03, by wenzelm
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
2007-06-03, by wenzelm
tuned Tactic signature;
2007-06-03, by wenzelm
removed obsolete Library.seq;
2007-06-03, by wenzelm

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

isabelle