| Wed, 30 Dec 2015 17:55:43 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:37:29 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| Thu, 06 Aug 2015 23:56:48 +0200 |
haftmann |
slight cleanup of lemmas
|
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
|
| Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
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
|
| Sun, 02 Nov 2014 17:13:28 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sun, 26 Oct 2014 19:11:16 +0100 |
haftmann |
eliminated redundancies;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:25:35 +0200 |
hoelzl |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 19:59:19 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:58 +0100 |
hoelzl |
HOL-NSA should only import Complex_Main
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 10:07:53 -0700 |
huffman |
remove unnecessary intermediate lemmas
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 07:16:47 -0700 |
huffman |
remove obsolete intermediate lemma complex_inverse_complex_split
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 18:47:55 -0700 |
huffman |
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 14:53:51 -0700 |
huffman |
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 10:05:52 -0700 |
huffman |
remove redundant lemmas expi_add and expi_zero
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Fri, 18 Dec 2009 19:00:11 -0800 |
huffman |
rename equals_zero_I to minus_unique (keep old name too)
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 16:58:23 +0200 |
haftmann |
power constraint needed, though
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:30 +0200 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 17:47:22 +0200 |
huffman |
move nonstandard analysis theories to NSA directory
|
file |
diff |
annotate
|