2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Merge
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-03 wenzelm 2015-11-03 tuned imports;
2015-10-29 eberlm 2015-10-29 added many small lemmas about setsum/setprod/powr/...
2015-10-26 paulson 2015-10-26 new lemmas about topology, etc., for Cauchy integral formula
2015-10-13 paulson 2015-10-13 new material on path_component_sets, inside, outside, etc. And more default simprules
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-07-28 paulson 2015-07-28 the Cauchy integral theorem and related material
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-28 paulson 2015-04-28 New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-04-11 paulson 2015-04-11 Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
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-04-01 paulson 2015-04-01 HOL Light Libraries for complex Arctan, Arcsin, Arccos
2015-03-31 paulson 2015-03-31 New material and binomial fix
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 new HOL Light material about exp, sin, cos
2015-03-18 paulson 2015-03-18 new file for complex transcendental functions