2009-05-13 chaieb Now deals with division
2009-05-12 haftmann updated keywords
2009-05-12 haftmann split Predicate_Compile examples into separate theory
2009-05-12 haftmann adapted to changes in module Code
2009-05-12 haftmann values is now a keyword
2009-05-12 haftmann merged
2009-05-12 haftmann transferred code generator preprocessor into separate module
2009-05-12 haftmann marginally tuned
2009-05-12 haftmann examples using code_pred
2009-05-12 haftmann added dummy values keyword
2009-05-12 haftmann tuned exception code
2009-05-12 chaieb A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination
2009-05-12 chaieb A decision method for universal multivariate real arithmetic with add
2009-05-12 chaieb Isolated decision procedure for noms and the general arithmetic solver
2009-05-12 chaieb Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
2009-05-12 huffman merged
2009-05-11 huffman use Pair/fst/snd instead of cpair/cfst/csnd
2009-05-11 huffman use Pair/fst/snd instead of cpair/cfst/csnd
2009-05-11 huffman move bifinite instance for product type from Cprod.thy to Bifinite.thy
2009-05-11 huffman new lemmas
2009-05-11 haftmann fixed merge accident
2009-05-11 haftmann merged
2009-05-11 haftmann avoid latex output problem
2009-05-11 haftmann merged
2009-05-11 bulwahn fixed code_pred command
2009-05-11 bulwahn Added pred_code command
2009-04-22 bulwahn added general preprocessing of equality in predicates for code generation
2009-05-11 haftmann merged
2009-05-11 haftmann merged
2009-05-11 haftmann mk_number replaces number_of
2009-05-11 haftmann qualified names for Lin_Arith tactics and simprocs
2009-05-11 haftmann tuned interface of Lin_Arith
2009-05-05 hoelzl optimized Approximation by precompiling approx_inequality
2009-04-29 hoelzl replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
2009-05-11 huffman merged
2009-05-11 huffman newline at end of file
2009-05-11 huffman simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
2009-05-11 huffman removed redundant instance declarations inat :: linorder
2009-05-11 haftmann merged
2009-05-11 haftmann proper error handling for malformed code equations
2009-05-11 haftmann corrected deletetion of code equations for constructors
2009-05-11 haftmann clarified matter of "proper" flag in code equations
2009-05-11 haftmann tuned interface of module Code_Unit
2009-05-11 haftmann clarified terminilogy concerning nbe equations
2009-05-11 haftmann simplified unoverload/overload policy in code generator preprocessor
2009-05-11 paulson Change to lowercase path names as directed by local pagemasters
2009-05-10 nipkow merged
2009-05-10 nipkow fixed HOLCF proofs
2009-05-09 haftmann merged
2009-05-09 haftmann interface changes in linarith.ML
2009-05-09 nipkow merged
2009-05-09 nipkow lemmas by Andreas Lochbihler
2009-05-08 nipkow merged
2009-05-08 nipkow merged
2009-05-08 nipkow more lemmas
2009-05-08 huffman rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2009-05-08 chaieb fixed theorem statement
2009-05-08 chaieb merged
2009-05-08 chaieb Generalized distributivity theorems of radicals over multiplication, division and inverses
2009-05-08 haftmann proper structure name
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip