2014-06-16 hoelzl 2014-06-16 lemmas about the moments of the normal distribution
2014-06-13 paulson 2014-06-13 NEWS
2014-06-13 hoelzl 2014-06-13 properties of normal distributed random variables (by Sudeep Kanav)
2014-06-13 nipkow 2014-06-13 announce Tree
2014-06-12 nipkow 2014-06-12 new theory of binary trees
2014-06-12 haftmann 2014-06-12 formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala
2014-06-12 nipkow 2014-06-12 merged
2014-06-12 nipkow 2014-06-12 added [simp]
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 renamed Sledgehammer options
2014-06-12 blanchet 2014-06-12 removed dead code
2014-06-12 blanchet 2014-06-12 reintroduced vital 'Thm.transfer'
2014-06-12 blanchet 2014-06-12 tuned dependencies
2014-06-12 blanchet 2014-06-12 updated docs
2014-06-12 blanchet 2014-06-12 added support for CVC4 in SMT2
2014-06-12 blanchet 2014-06-12 don't ask proof-disabled solvers to do proofs
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
2014-06-12 blanchet 2014-06-12 made CVC3 work with SMT2 stack
2014-06-12 hoelzl 2014-06-12 properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
2014-06-11 hoelzl 2014-06-11 clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
2014-06-12 haftmann 2014-06-12 uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
2014-06-12 blanchet 2014-06-12 adapted examples to changes in SMT triggers
2014-06-12 blanchet 2014-06-12 reduces Sledgehammer dependencies
2014-06-12 blanchet 2014-06-12 eliminate dependency of SMT2 module on 'list'
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 removed subsumed record-related code, now that records are registered as 'ctr_sugar'
2014-06-12 blanchet 2014-06-12 made lookup more robust in the face of missing (dummy) case constant
2014-06-12 blanchet 2014-06-12 use 'ctr_sugar' abstraction in SMT(2)
2014-06-12 blanchet 2014-06-12 register record extensions as freely generated types
2014-06-11 haftmann 2014-06-11 mixin definitions are within scope of "for"s of import expression
2014-06-11 haftmann 2014-06-11 proper proof context transfer wrt. background theory avoids ad-hoc restore operation
2014-06-11 blanchet 2014-06-11 refactoring
2014-06-11 blanchet 2014-06-11 moved generic code further up
2014-06-11 blanchet 2014-06-11 tuned code
2014-06-11 blanchet 2014-06-11 factor out SMT-LIB 2 type/term parsing from Z3-specific code
2014-06-11 blanchet 2014-06-11 simplify slightly ATP proof generated for Z3
2014-06-11 steckerm 2014-06-11 tuned whitespaces
2014-06-11 blanchet 2014-06-11 updated contributors to include students
2014-06-11 blanchet 2014-06-11 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
2014-06-11 blanchet 2014-06-11 adapted SMT examples to new, corrected handling of 'typedef'
2014-06-11 blanchet 2014-06-11 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
2014-06-11 blanchet 2014-06-11 updated NEWS slightly
2014-06-11 blanchet 2014-06-11 updated docs w.r.t. Z3
2014-06-11 blanchet 2014-06-11 rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
2014-06-11 blanchet 2014-06-11 removed '_new' sufffix in SMT2 solver names (in some cases)
2014-06-11 blanchet 2014-06-11 removed old SMT module from Sledgehammer
2014-06-11 blanchet 2014-06-11 got rid of 'listF' example, which is now subsumed by the real 'list' type
2014-06-10 blanchet 2014-06-10 changed syntax of map: and rel: arguments to BNF-based datatypes
2014-06-10 blanchet 2014-06-10 tuning
2014-06-10 blanchet 2014-06-10 updated Z3 certificates
2014-06-10 blanchet 2014-06-10 generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction
2014-06-10 blanchet 2014-06-10 tuning
2014-06-10 Andreas Lochbihler 2014-06-10 add type class instances for unit
2014-06-10 blanchet 2014-06-10 use 'where' clause for selector default value syntax
2014-06-10 blanchet 2014-06-10 tuning
2014-06-09 nipkow 2014-06-09 added List.union
2014-06-09 nipkow 2014-06-09 Sup/Inf on functions decoupled from complete_lattice.
2014-06-08 haftmann 2014-06-08 tuned data structure
2014-06-08 haftmann 2014-06-08 recovered level-free fishing for locale, accidentally lost in dce365931721