Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
Mon, 31 Aug 2015 21:28:08 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
Thu, 06 Aug 2015 23:56:48 +0200 |
haftmann |
slight cleanup of lemmas
|
file |
diff |
annotate
|
Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Tue, 14 Jul 2015 13:48:03 +0200 |
hoelzl |
generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
|
file |
diff |
annotate
|
Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
Mon, 25 May 2015 22:11:43 +0200 |
wenzelm |
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
|
file |
diff |
annotate
|
Sun, 03 May 2015 16:45:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 07 May 2015 15:34:28 +0200 |
hoelzl |
generalized tends over powr; added DERIV rule for powr
|
file |
diff |
annotate
|
Thu, 30 Apr 2015 15:28:01 +0100 |
paulson |
tidying some messy proofs
|
file |
diff |
annotate
|
Wed, 29 Apr 2015 14:04:22 +0100 |
paulson |
Tidying. Improved simplification for numerals, esp in exponents.
|
file |
diff |
annotate
|
Tue, 28 Apr 2015 16:23:38 +0100 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
file |
diff |
annotate
|
Tue, 21 Apr 2015 17:19:00 +0100 |
paulson |
New material, mostly about limits. Consolidation.
|
file |
diff |
annotate
|
Sun, 12 Apr 2015 11:33:19 +0200 |
hoelzl |
move filters to their own theory
|
file |
diff |
annotate
|
Sun, 12 Apr 2015 16:04:53 +0200 |
hoelzl |
fix latex in Transcendental
|
file |
diff |
annotate
|
Sat, 11 Apr 2015 22:18:33 +0100 |
paulson |
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
|
file |
diff |
annotate
|
Sat, 11 Apr 2015 11:56:40 +0100 |
paulson |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
file |
diff |
annotate
|
Wed, 01 Apr 2015 14:08:17 +0100 |
paulson |
arcsin and arccos lemmas
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 16:48:48 +0100 |
paulson |
rationalised and generalised some theorems concerning abs and x^2.
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 15:00:03 +0100 |
paulson |
New material and binomial fix
|
file |
diff |
annotate
|
Thu, 19 Mar 2015 14:24:51 +0000 |
paulson |
New material for complex sin, cos, tan, Ln, also some reorganisation
|
file |
diff |
annotate
|
Wed, 18 Mar 2015 17:23:22 +0000 |
paulson |
new HOL Light material about exp, sin, cos
|
file |
diff |
annotate
|
Wed, 18 Mar 2015 14:13:27 +0000 |
paulson |
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
|
file |
diff |
annotate
|
Tue, 17 Mar 2015 12:23:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
Fri, 13 Mar 2015 12:44:16 +0100 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
Tue, 10 Mar 2015 16:12:35 +0000 |
paulson |
renaming HOL/Fact.thy -> Binomial.thy
|
file |
diff |
annotate
|
Mon, 09 Mar 2015 16:28:19 +0000 |
paulson |
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
|
file |
diff |
annotate
|
Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
Thu, 05 Mar 2015 17:30:29 +0000 |
paulson |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 23:31:04 +0100 |
nipkow |
Removed the obsolete functions "natfloor" and "natceiling"
|
file |
diff |
annotate
|
Wed, 12 Nov 2014 17:36:36 +0100 |
immler |
added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
|
file |
diff |
annotate
|
Wed, 12 Nov 2014 17:36:25 +0100 |
immler |
code equation for powr
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
Thu, 30 Oct 2014 21:02:01 +0100 |
haftmann |
more simp rules concerning dvd and even/odd
|
file |
diff |
annotate
|
Tue, 21 Oct 2014 21:10:44 +0200 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
Mon, 20 Oct 2014 18:33:14 +0200 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
Mon, 20 Oct 2014 07:45:58 +0200 |
haftmann |
augmented and tuned facts on even/odd and division
|
file |
diff |
annotate
|
Sun, 19 Oct 2014 18:05:26 +0200 |
haftmann |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
file |
diff |
annotate
|
Mon, 13 Oct 2014 18:55:05 +0200 |
immler |
relaxed class constraints for exp
|
file |
diff |
annotate
|
Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
Fri, 06 Jun 2014 12:36:06 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Fri, 30 May 2014 14:55:10 +0200 |
hoelzl |
introduce more powerful reindexing rules for big operators
|
file |
diff |
annotate
|
Tue, 20 May 2014 19:24:39 +0200 |
hoelzl |
add various lemmas
|
file |
diff |
annotate
|
Tue, 13 May 2014 22:14:12 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 13:15:21 +0200 |
hoelzl |
generalize ln/log_powr; add log_base_powr/pow
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|