src/HOL/Real/HahnBanach/HahnBanach.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-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-27 ballarin 2005-05-27 Locale expressions: rename with optional mixfix syntax.
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-05-07 bauerg 2004-05-07 replaced Aux.thy by RealLemmas.thy
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-11 ballarin 2003-12-11 Change to prune_prems in Pure/Isar/locale.ML.
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed.
2002-08-29 wenzelm 2002-08-29 tuned;
2002-08-22 wenzelm 2002-08-22 updated to use locales (still some rough edges);
2001-11-02 paulson 2001-11-02 Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2000-12-16 wenzelm 2000-12-16 tuned HOL/Real/HahnBanach;
2000-11-03 wenzelm 2000-11-03 adapted "obtain" proofs;
2000-09-07 wenzelm 2000-09-07 linorder_cases;
2000-08-17 wenzelm 2000-08-17 renamed 'RS' to 'THEN'; 'symmetric' attribute;
2000-08-09 bauerg 2000-08-09 tuned;
2000-08-03 wenzelm 2000-08-03 tuned;
2000-07-30 wenzelm 2000-07-30 adapted obtain; tuned;
2000-07-20 wenzelm 2000-07-20 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-07-06 bauerg 2000-07-06 removed sorry;
2000-07-06 bauerg 2000-07-06 completed TYPES version of HahnBanach;
2000-06-04 wenzelm 2000-06-04 removed explicit terminator (";");
2000-06-01 fleuriot 2000-06-01 Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added.
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-08 wenzelm 2000-05-08 replaced rabs by overloaded abs;
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-04-05 wenzelm 2000-04-05 fixed goal selection;
2000-01-06 wenzelm 2000-01-06 obtain: renamed 'in' to 'where';
2000-01-05 wenzelm 2000-01-05 oops';
2000-01-05 wenzelm 2000-01-05 oops;
2000-01-05 wenzelm 2000-01-05 tuned;
2000-01-03 bauerg 2000-01-03 small changes;
1999-10-29 wenzelm 1999-10-29 final update by Gertrud Bauer;
1999-10-25 wenzelm 1999-10-25 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);