| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 09:31:23 -0700 |
huffman |
add simp rules for isCont
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 14:50:24 -0700 |
huffman |
remove duplicate lemma disjoint_iff
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 13:05:56 -0700 |
huffman |
modify euclidean_space class to include basis set
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 09:11:15 -0700 |
huffman |
remove lemma stupid_ext
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 17:02:03 -0700 |
huffman |
follow standard naming scheme for sgn_vec_def
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 13:13:37 -0700 |
huffman |
more uniform naming scheme for finite cartesian product type and related theorems
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 10:13:16 -0700 |
huffman |
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 19:35:57 +0200 |
hoelzl |
Rewrite the Probability theory.
|
file |
diff |
annotate
|
| Tue, 04 May 2010 10:42:47 -0700 |
huffman |
make (f -- a --> x) an abbreviation for (f ---> x) (at a)
|
file |
diff |
annotate
|
| Tue, 04 May 2010 10:06:05 -0700 |
huffman |
make (X ----> L) an abbreviation for (X ---> L) sequentially
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 09:17:25 -0700 |
huffman |
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 07:22:01 -0700 |
huffman |
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 13:32:55 +0100 |
wenzelm |
more precise syntax antiquotations;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 21:04:17 +0100 |
wenzelm |
binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 20:55:12 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:19:58 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Mon, 25 Jan 2010 16:56:24 +0100 |
hoelzl |
Replaced vec1 and dest_vec1 by abbreviation.
|
file |
diff |
annotate
|
| Thu, 07 Jan 2010 18:56:39 +0100 |
hoelzl |
finite annotation on cartesian product is now implicit.
|
file |
diff |
annotate
|
| Thu, 07 Jan 2010 17:43:35 +0100 |
hoelzl |
added syntax translation to automatically add finite typeclass to index type of cartesian product type
|
file |
diff |
annotate
|
| Wed, 06 Jan 2010 13:07:30 +0100 |
himmelma |
Made finite cartesian products finite
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 15:03:23 +0100 |
hoelzl |
removed hassize predicate
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 13:23:18 +0200 |
himmelma |
distinguished session for multivariate analysis
|
file |
diff |
annotate
|