Wed, 30 Dec 2015 18:03:23 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
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
|
Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
Mon, 07 Dec 2015 16:44:26 +0000 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
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
|
Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
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
|
Sun, 12 Apr 2015 11:34:16 +0200 |
hoelzl |
replace Filters in NSA by HOL-Filters
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 17:13:28 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Wed, 29 Oct 2014 10:35:00 +0100 |
wenzelm |
more standard theory name;
|
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
|
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
|
Thu, 20 Mar 2014 12:43:48 +0000 |
paulson |
fixing messy proofs
|
file |
diff |
annotate
|
Wed, 19 Mar 2014 17:06:02 +0000 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
Tue, 26 Mar 2013 12:20:55 +0100 |
hoelzl |
merge RComplete into RealDef
|
file |
diff |
annotate
|
Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
Thu, 17 Nov 2011 07:55:09 +0100 |
huffman |
simplify implementation of approx_reorient_simproc
|
file |
diff |
annotate
|
Thu, 17 Nov 2011 07:31:37 +0100 |
huffman |
name simp theorems st_0 and st_1
|
file |
diff |
annotate
|
Sat, 17 Sep 2011 00:37:21 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Thu, 13 Jan 2011 23:50:16 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
Mon, 06 Sep 2010 19:13:10 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
Sun, 09 May 2010 23:57:56 -0700 |
huffman |
real_mult_commute -> mult_commute
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 15:37:50 +0200 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 11:34:17 +0200 |
haftmann |
class division_ring_inverse_zero
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
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
|
Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
Thu, 23 Jul 2009 23:12:21 +0200 |
wenzelm |
more @{theory} antiquotations;
|
file |
diff |
annotate
|
Fri, 05 Jun 2009 00:24:47 -0700 |
huffman |
fix type of hnorm
|
file |
diff |
annotate
|
Tue, 28 Apr 2009 15:50:30 +0200 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
file |
diff |
annotate
|
Tue, 24 Feb 2009 08:20:14 -0800 |
huffman |
fix lemma hypreal_hnorm_def
|
file |
diff |
annotate
|
Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
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
|