src/HOL/Real/HahnBanach/Bounds.thy
2008-07-15 wenzelm 2008-07-15 modernized specifications and proofs; tuned document;
2008-07-15 ballarin 2008-07-15 Removed uses of context element includes.
2007-12-10 haftmann 2007-12-10 tuned header
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-05-27 wenzelm 2006-05-27 tuned;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-22 wenzelm 2004-04-22 constdefs: proper order;
2002-08-22 wenzelm 2002-08-22 updated to use locales (still some rough edges);
2000-12-16 wenzelm 2000-12-16 tuned HOL/Real/HahnBanach;
2000-08-03 wenzelm 2000-08-03 tuned;
2000-07-17 bauerg 2000-07-17 tuded presentation;
2000-07-17 bauerg 2000-07-17 - xsymbols for \<noteq> \<notin> \<in> \<exists> \<forall> \<and> \<inter> \<union> \<Union> - vector space type of {plus, minus, zero}, overload 0 in vector space - syntax |.| and ||.||
2000-06-04 wenzelm 2000-06-04 removed explicit terminator (";");
2000-04-01 wenzelm 2000-04-01 tuned presentation;
2000-03-26 wenzelm 2000-03-26 tuned presentation;
1999-10-29 wenzelm 1999-10-29 final update by Gertrud Bauer;
1999-10-22 wenzelm 1999-10-22 HahnBanach update by Gertrud Bauer;
1999-10-08 wenzelm 1999-10-08 update from Gertrud;
1999-09-29 wenzelm 1999-09-29 update from Gertrud;
1999-09-21 wenzelm 1999-09-21 accomodate refined facts handling;
1999-09-10 wenzelm 1999-09-10 The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich);