| Mon, 01 Dec 2008 15:36:48 -0800 |
huffman |
clean up imports related to ContNotDenum
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 22:34:25 +0100 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 11:27:00 +0100 |
chaieb |
Added trivial theorems aboud cmod
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 22:34:03 +0100 |
haftmann |
instantiation target
|
file |
diff |
annotate
|
| Tue, 11 Dec 2007 10:23:03 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Sun, 02 Sep 2007 23:36:21 +0200 |
huffman |
fix sgn_div_norm class
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 01:21:48 +0200 |
nipkow |
final(?) iteration of sgn saga.
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 16:42:39 +0200 |
huffman |
declare complex_diff as simp rule
|
file |
diff |
annotate
|
| Wed, 30 May 2007 01:46:05 +0200 |
huffman |
cleaned up proofs; reorganized sections; removed redundant lemmas
|
file |
diff |
annotate
|
| Tue, 29 May 2007 20:53:13 +0200 |
huffman |
use new-style instance declarations
|
file |
diff |
annotate
|
| Tue, 29 May 2007 20:31:53 +0200 |
huffman |
instance complex :: banach
|
file |
diff |
annotate
|
| Mon, 14 May 2007 20:14:31 +0200 |
huffman |
generalized sgn function to work on any real normed vector space
|
file |
diff |
annotate
|
| Mon, 14 May 2007 18:03:25 +0200 |
huffman |
tuned
|
file |
diff |
annotate
|
| Sun, 13 May 2007 20:05:42 +0200 |
huffman |
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
|
file |
diff |
annotate
|
| Thu, 10 May 2007 03:11:03 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Thu, 10 May 2007 03:07:26 +0200 |
huffman |
lemmas iszero_(h)complex_number_of are no longer needed
|
file |
diff |
annotate
|
| Wed, 09 May 2007 18:26:40 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Wed, 09 May 2007 01:56:59 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Wed, 09 May 2007 01:26:04 +0200 |
huffman |
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
|
file |
diff |
annotate
|
| Tue, 08 May 2007 05:30:10 +0200 |
huffman |
clean up complex norm proofs, remove redundant lemmas
|
file |
diff |
annotate
|
| Mon, 07 May 2007 23:07:04 +0200 |
huffman |
clean up RealVector classes
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 01:06:12 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 19:04:13 +0200 |
huffman |
rearranged axioms and simp rules for scaleR
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 03:05:28 +0200 |
huffman |
instance complex :: real_normed_field; cleaned up
|
file |
diff |
annotate
|
| Sun, 17 Sep 2006 16:42:38 +0200 |
huffman |
norm_one is now proved from other class axioms
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 23:46:38 +0200 |
huffman |
complex_of_real abbreviates of_real::real=>complex;
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 19:14:37 +0200 |
huffman |
add instance for real_algebra_1 and real_normed_div_algebra
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:01:57 +0200 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
| Mon, 01 Mar 2004 13:51:21 +0100 |
paulson |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Thu, 05 Feb 2004 10:45:28 +0100 |
paulson |
tidying up, especially the Complex numbers
|
file |
diff |
annotate
|
| Tue, 03 Feb 2004 15:58:31 +0100 |
paulson |
further tidying of the complex numbers
|
file |
diff |
annotate
|
| Tue, 03 Feb 2004 11:06:36 +0100 |
paulson |
tidying of the complex numbers
|
file |
diff |
annotate
|
| Tue, 13 Jan 2004 10:37:52 +0100 |
paulson |
types complex and hcomplex are now instances of class ringpower:
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
| Tue, 06 Jan 2004 10:40:15 +0100 |
paulson |
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 21:47:07 +0100 |
paulson |
conversion of Real/PReal to Isar script;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 10:06:32 +0100 |
paulson |
tweaking of lemmas in RealDef, RealOrd
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 16:53:33 +0100 |
paulson |
converting Complex/Complex.ML to Isar
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:22:31 +0200 |
paulson |
new session Complex for the complex numbers
|
file |
diff |
annotate
|