2009-05-11 haftmann 2009-05-11 qualified names for Lin_Arith tactics and simprocs
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-05-05 hoelzl 2009-05-05 optimized Approximation by precompiling approx_inequality
2009-04-29 hoelzl 2009-04-29 replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
2009-05-11 huffman 2009-05-11 merged
2009-05-11 huffman 2009-05-11 newline at end of file
2009-05-11 huffman 2009-05-11 simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
2009-05-11 huffman 2009-05-11 removed redundant instance declarations inat :: linorder
2009-05-11 haftmann 2009-05-11 merged
2009-05-11 haftmann 2009-05-11 proper error handling for malformed code equations
2009-05-11 haftmann 2009-05-11 corrected deletetion of code equations for constructors
2009-05-11 haftmann 2009-05-11 clarified matter of "proper" flag in code equations
2009-05-11 haftmann 2009-05-11 tuned interface of module Code_Unit
2009-05-11 haftmann 2009-05-11 clarified terminilogy concerning nbe equations
2009-05-11 haftmann 2009-05-11 simplified unoverload/overload policy in code generator preprocessor
2009-05-11 paulson 2009-05-11 Change to lowercase path names as directed by local pagemasters
2009-05-10 nipkow 2009-05-10 merged
2009-05-10 nipkow 2009-05-10 fixed HOLCF proofs
2009-05-09 haftmann 2009-05-09 merged
2009-05-09 haftmann 2009-05-09 interface changes in linarith.ML
2009-05-09 nipkow 2009-05-09 merged
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-05-08 nipkow 2009-05-08 merged
2009-05-08 nipkow 2009-05-08 merged
2009-05-08 nipkow 2009-05-08 more lemmas
2009-05-08 huffman 2009-05-08 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2009-05-08 chaieb 2009-05-08 fixed theorem statement
2009-05-08 chaieb 2009-05-08 merged
2009-05-08 chaieb 2009-05-08 Generalized distributivity theorems of radicals over multiplication, division and inverses
2009-05-08 haftmann 2009-05-08 proper structure name
2009-05-08 haftmann 2009-05-08 localized (complete) partial order classes
2009-05-08 haftmann 2009-05-08 dropped legacy ml theorem binding
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-08 haftmann 2009-05-08 generalized simproc for mod
2009-05-08 haftmann 2009-05-08 explicit method linarith
2009-05-08 haftmann 2009-05-08 moved int_factor_simprocs.ML to theory Int
2009-05-07 haftmann 2009-05-07 treat frees driectly by the LCF kernel
2009-05-07 haftmann 2009-05-07 dropped explicit suppport for frees in evaluation conversion stack
2009-05-07 haftmann 2009-05-07 no need for explicit delete declaration
2009-05-07 haftmann 2009-05-07 better to have distinguished class for preorders
2009-05-07 haftmann 2009-05-07 added theory for explicit equivalence relation in preorders
2009-05-07 haftmann 2009-05-07 explicit type_name antiquotations
2009-05-07 haftmann 2009-05-07 explicit type arguments in constants
2009-05-06 haftmann 2009-05-06 merged
2009-05-06 haftmann 2009-05-06 robustifed infrastructure for complex term syntax during code generation
2009-05-06 haftmann 2009-05-06 proper structures for list and string code generation stuff
2009-05-06 haftmann 2009-05-06 explicit type arguments in constants
2009-05-06 haftmann 2009-05-06 confine term setup to Eval serialiser
2009-05-06 haftmann 2009-05-06 adaptation replaces adaption
2009-05-06 haftmann 2009-05-06 refined HOL string theories and corresponding ML fragments
2009-05-06 haftmann 2009-05-06 adaptation replaces adaption
2009-05-06 haftmann 2009-05-06 explicit type arguments in constants
2009-05-06 haftmann 2009-05-06 refined HOL string theories and corresponding ML fragments
2009-05-06 haftmann 2009-05-06 tuned description of overloading
2009-05-06 haftmann 2009-05-06 confine term setup to Eval serialiser
2009-05-06 haftmann 2009-05-06 updated generated file
2009-05-06 nipkow 2009-05-06 new lemmas
2009-05-06 nipkow 2009-05-06 merged
2009-05-06 Timothy Bourke 2009-05-06 Prototype introiff option for find_theorems. This feature was suggested by Jeremy Avigad / Tobias Nipkow. It adds an introiff keyword for find_theorems that returns, in addition to the usual results for intro, any theorems of the form ([| ... |] ==> (P = Q)) where either P or Q matches the conclusions of the current goal. Such theorems can be made introduction rules with [THEN iffDx]. The current patch is for evaluation only. It assumes an (op = : 'a -> 'a -> bool) operator, which is specific to HOL. It is not clear how this should be generalised.