| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 23:46:33 +0200 |
huffman |
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
|
file |
diff |
annotate
|
| Tue, 26 Aug 2008 23:49:46 +0200 |
huffman |
move real_vector class proofs into vector_space and group_hom locales
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 16:56:20 +0200 |
huffman |
instance real_field < field_char_0;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:03:25 +0200 |
haftmann |
re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
|
file |
diff |
annotate
|
| Thu, 10 Jul 2008 07:07:54 +0200 |
huffman |
instance real_field < field_char_0
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 19:35:43 +0200 |
huffman |
use begin and end for proofs in locales
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:11:57 +0200 |
haftmann |
cleaned up some code generator configuration
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 08:04:28 +0200 |
haftmann |
added first version of user-space type system for class target
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:43 +0200 |
haftmann |
introduced classes
|
file |
diff |
annotate
|
| Sun, 02 Sep 2007 23:36:21 +0200 |
huffman |
fix sgn_div_norm class
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 16:12:50 +0200 |
wenzelm |
removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 01:21:48 +0200 |
nipkow |
final(?) iteration of sgn saga.
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 20:49:04 +0200 |
huffman |
add axclass semiring_char_0 for types where of_nat is injective
|
file |
diff |
annotate
|
| Wed, 30 May 2007 02:41:26 +0200 |
huffman |
simplify names of locale interpretations
|
file |
diff |
annotate
|
| Tue, 29 May 2007 18:19:56 +0200 |
huffman |
interpretation bounded_linear_divide
|
file |
diff |
annotate
|
| Mon, 28 May 2007 04:22:44 +0200 |
huffman |
interpretations additive_scaleR_left, additive_scaleR_right
|
file |
diff |
annotate
|
| Mon, 14 May 2007 20:48:32 +0200 |
huffman |
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
|
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
|
| Sat, 12 May 2007 18:16:30 +0200 |
huffman |
add lemma additive.setsum
|
file |
diff |
annotate
|
| Thu, 10 May 2007 03:00:15 +0200 |
huffman |
instance real_algebra_1 < ring_char_0
|
file |
diff |
annotate
|
| Wed, 09 May 2007 22:14:26 +0200 |
huffman |
add lemma norm_diff_ineq; shorten other proofs
|
file |
diff |
annotate
|
| Wed, 09 May 2007 00:27:36 +0200 |
huffman |
add lemmas norm_add_less, norm_mult_less
|
file |
diff |
annotate
|
| Tue, 08 May 2007 18:23:37 +0200 |
huffman |
add lemmas norm_number_of, norm_of_int, norm_of_nat
|
file |
diff |
annotate
|
| Tue, 08 May 2007 04:55:19 +0200 |
huffman |
add lemma abs_norm_cancel
|
file |
diff |
annotate
|
| Mon, 07 May 2007 23:07:04 +0200 |
huffman |
clean up RealVector classes
|
file |
diff |
annotate
|
| Wed, 11 Apr 2007 19:42:43 +0200 |
huffman |
new class syntax for scaleR and norm classes
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 21:51:08 +0200 |
huffman |
interpretation bounded_linear_of_real
|
file |
diff |
annotate
|
| Wed, 14 Mar 2007 21:40:28 +0100 |
huffman |
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 00:02:53 +0100 |
huffman |
remove uses of scaleR infix syntax; add lemma Reals_number_of
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 18:30:10 +0200 |
huffman |
add lemmas norm_not_less_zero, norm_le_zero_iff
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:47 +0200 |
wenzelm |
tuned definitions/proofs;
|
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 01:48:30 +0200 |
huffman |
add lemmas about of_real and power
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 00:52:59 +0200 |
huffman |
add lemmas of_int_in_Reals, of_nat_in_Reals
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 07:14:02 +0200 |
huffman |
real_norm_def [simp]
|
file |
diff |
annotate
|
| Fri, 22 Sep 2006 23:17:39 +0200 |
huffman |
add lemma norm_power
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 06:22:26 +0200 |
huffman |
added classes real_div_algebra and real_field; added lemmas
|
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 19:12:03 +0200 |
huffman |
define new constant of_real for class real_algebra_1;
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 02:35:58 +0200 |
huffman |
add theorem norm_diff_triangle_ineq
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 03:25:17 +0200 |
huffman |
remove conflicting norm syntax
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 06:44:45 +0200 |
huffman |
formalization of vector spaces and algebras over the real numbers
|
file |
diff |
annotate
|