src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
Tue, 04 May 2010 10:42:47 -0700 huffman make (f -- a --> x) an abbreviation for (f ---> x) (at a)
Tue, 04 May 2010 10:06:05 -0700 huffman make (X ----> L) an abbreviation for (X ---> L) sequentially
Thu, 29 Apr 2010 09:17:25 -0700 huffman move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
Thu, 29 Apr 2010 07:22:01 -0700 huffman remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
Sat, 27 Feb 2010 13:32:55 +0100 wenzelm more precise syntax antiquotations;
Sun, 21 Feb 2010 21:04:17 +0100 wenzelm binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
Sun, 21 Feb 2010 20:55:12 +0100 wenzelm tuned headers;
Thu, 11 Feb 2010 22:19:58 +0100 wenzelm modernized translations;
Mon, 25 Jan 2010 16:56:24 +0100 hoelzl Replaced vec1 and dest_vec1 by abbreviation.
Thu, 07 Jan 2010 18:56:39 +0100 hoelzl finite annotation on cartesian product is now implicit.
Thu, 07 Jan 2010 17:43:35 +0100 hoelzl added syntax translation to automatically add finite typeclass to index type of cartesian product type
Wed, 06 Jan 2010 13:07:30 +0100 himmelma Made finite cartesian products finite
Mon, 16 Nov 2009 15:03:23 +0100 hoelzl removed hassize predicate
Fri, 23 Oct 2009 13:23:18 +0200 himmelma distinguished session for multivariate analysis
less more (0) tip