nik [Tue, 30 Aug 2011 14:12:55 +0200] rev 45449
added generation of induction rules
huffman [Mon, 29 Aug 2011 13:50:47 -0700] rev 45448
simplify some proofs
wenzelm [Mon, 29 Aug 2011 22:10:08 +0200] rev 45447
merged
wenzelm [Mon, 29 Aug 2011 21:55:49 +0200] rev 45446
actual auto loading of required files;
eliminated File_Store in favour of Thy_Load;
tuned;
wenzelm [Mon, 29 Aug 2011 16:38:56 +0200] rev 45445
some dialog for auto loading of required files (still inactive);
wenzelm [Mon, 29 Aug 2011 16:28:51 +0200] rev 45444
invoke in Swing thread to make double sure;
huffman [Mon, 29 Aug 2011 08:31:09 -0700] rev 45443
Product_Vector.thy: clean up some proofs
huffman [Sun, 28 Aug 2011 20:56:49 -0700] rev 45442
move class perfect_space into RealVector.thy;
use not_open_singleton as perfect_space class axiom;
generalize some lemmas to class perfect_space;
huffman [Sun, 28 Aug 2011 16:28:07 -0700] rev 45441
generalize LIM_zero lemmas to arbitrary filters
huffman [Sun, 28 Aug 2011 09:22:42 -0700] rev 45440
merged