2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-03-30 eberlm 2015-03-30 exposed approximation in ML
2015-03-19 paulson 2015-03-19 New material for complex sin, cos, tan, Ln, also some reorganisation
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-09 paulson 2015-03-09 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-12 immler 2014-11-12 added quickcheck[approximation]
2014-11-12 immler 2014-11-12 disjunction and conjunction for forms
2014-11-12 immler 2014-11-12 truncate intermediate results in horner to improve performance of approximate; more efficient truncated addition float_plus_up/float_plus_down
2014-11-12 immler 2014-11-12 simplified computations based on round_up by reducing to round_down; more general round_up_le1, round_up_less1, round_down_ge1, round_up_le0
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-19 haftmann 2014-10-19 prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-09 haftmann 2014-05-09 prefer separate command for approximation
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-05-01 haftmann 2014-05-01 separate ML module
2014-04-14 hoelzl 2014-04-14 added divide_nonneg_nonneg and co; made it a simp rule
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 generalize ln/log_powr; add log_base_powr/pow
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-04 paulson 2014-04-04 divide_minus_left divide_minus_right are in field_simps but are not default simprules
2014-04-03 hoelzl 2014-04-03 fix #0556204bc230
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-03-18 huffman 2014-03-18 adapt to Isabelle/c726ecfb22b6
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-02-15 wenzelm 2014-02-15 removed dead code; tuned;
2014-02-14 blanchet 2014-02-14 merged '' and 'Option.map_option'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
2013-12-16 immler 2013-12-16 additional definitions and lemmas for Float
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-05 hoelzl 2013-11-05 tuned proofs in Approximation
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-06-02 haftmann 2013-06-02 make reification part of HOL
2013-05-31 haftmann 2013-05-31 decomposed reflection steps into conversions; deholified reification procedure; prefer Subgoal.FOCUS over SUBGOAL
2013-05-31 haftmann 2013-05-31 dropped vacuous prefix
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-05-20 wenzelm 2013-05-20 proper context;
2013-04-21 haftmann 2013-04-21 combined reify_data.ML into reflection.ML; attempt to establish a more accessible and more consistent terminology; more ML code in ML file rather than setup theory; ML slightly tuned wrt. Isabelle coding conventions
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-03-26 wenzelm 2013-03-26 tuned session specification;
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-09-13 wenzelm 2012-09-13 tuned proofs;
2012-04-20 hoelzl 2012-04-20 hide code generation facts in the Float theory, they are only exported for Approximation
2012-04-19 hoelzl 2012-04-19 use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
2012-04-18 hoelzl 2012-04-18 use lifting to introduce floating point numbers