2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-05-16 bulwahn 2009-05-16 merged
2009-05-16 bulwahn 2009-05-16 added collection of simplification rules of recursive functions for quickcheck
2009-05-16 bulwahn 2009-05-16 merged
2009-05-15 bulwahn 2009-05-15 added predicate transformation function for code generation
2009-05-15 bulwahn 2009-05-15 added predicate transformation function for code generation
2009-05-16 nipkow 2009-05-16 proof tuned
2009-05-16 nipkow 2009-05-16 merged
2009-05-16 nipkow 2009-05-16 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
2009-05-15 huffman 2009-05-15 merged
2009-05-15 huffman 2009-05-15 continuity proofs for approx function on deflations; lemma cast_below_imp_below
2009-05-12 huffman 2009-05-12 allow lazy domain arguments to have class cpo
2009-05-12 huffman 2009-05-12 add cpo_type function
2009-05-12 huffman 2009-05-12 fix domain package parsing of lhs sort constraints
2009-05-12 huffman 2009-05-12 export quiet_mode and trace_domain refs for domain package
2009-05-15 nipkow 2009-05-15 new lemma
2009-05-14 haftmann 2009-05-14 merged
2009-05-14 haftmann 2009-05-14 merged
2009-05-14 haftmann 2009-05-14 merged module code_unit.ML into code.ML
2009-05-14 haftmann 2009-05-14 monomorphic code generation for power operations
2009-05-14 haftmann 2009-05-14 preprocessing must consider eq
2009-05-14 haftmann 2009-05-14 quickcheck size starts with 0
2009-05-14 haftmann 2009-05-14 strip sorts while checking pattern subsumption
2009-05-14 haftmann 2009-05-14 rewrite op = == eq handled by simproc
2009-05-14 haftmann 2009-05-14 updated generated document
2009-05-14 nipkow 2009-05-14 merged
2009-05-14 nipkow 2009-05-14 Cleaned up Parity a little
2009-05-14 berghofe 2009-05-14 merged
2009-05-13 berghofe 2009-05-13 merged
2009-05-13 berghofe 2009-05-13 Cleaned up code of function test_term.
2009-05-14 haftmann 2009-05-14 dropped accidental debug messages
2009-05-14 haftmann 2009-05-14 adapted code tutorial to recent changes in code
2009-05-13 haftmann 2009-05-13 more permissive wrt. overloaded constants
2009-05-13 haftmann 2009-05-13 merged
2009-05-13 haftmann 2009-05-13 tuned construction of term_of instances
2009-05-13 haftmann 2009-05-13 tuned construction of term_of instances
2009-05-13 haftmann 2009-05-13 dropped legacy operations
2009-05-13 haftmann 2009-05-13 tuned construction of typerep instances
2009-05-13 haftmann 2009-05-13 tuned and generalized construction of code equations for eq; tuned interface
2009-05-13 haftmann 2009-05-13 added abstract operations for typerep/term_of
2009-05-13 haftmann 2009-05-13 tuned and generalized construction of code equations for eq
2009-05-13 haftmann 2009-05-13 dropped sort constraint on predicate equality
2009-05-13 haftmann 2009-05-13 itself is instance of eq
2009-05-13 chaieb 2009-05-13 Now deals with division
2009-05-12 haftmann 2009-05-12 updated keywords
2009-05-12 haftmann 2009-05-12 split Predicate_Compile examples into separate theory
2009-05-12 haftmann 2009-05-12 adapted to changes in module Code
2009-05-12 haftmann 2009-05-12 values is now a keyword
2009-05-12 haftmann 2009-05-12 merged
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-05-12 haftmann 2009-05-12 marginally tuned
2009-05-12 haftmann 2009-05-12 examples using code_pred
2009-05-12 haftmann 2009-05-12 added dummy values keyword
2009-05-12 haftmann 2009-05-12 tuned exception code
2009-05-12 chaieb 2009-05-12 A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination
2009-05-12 chaieb 2009-05-12 A decision method for universal multivariate real arithmetic with add ition, multiplication and ordering using semidefinite programming
2009-05-12 chaieb 2009-05-12 Isolated decision procedure for noms and the general arithmetic solver
2009-05-12 chaieb 2009-05-12 Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
2009-05-11 huffman 2009-05-11 merged
2009-05-11 huffman 2009-05-11 use Pair/fst/snd instead of cpair/cfst/csnd