src/HOL/Real/HahnBanach/Subspace.thy
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
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;
2006-01-15 wenzelm 2006-01-15 prefer ex1I over ex_ex1I in single-step reasoning;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-12-25 paulson 2003-12-25 re-organized some hyperreal and real lemmas
2003-11-06 ballarin 2003-11-06 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.
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;
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2000-12-16 wenzelm 2000-12-16 tuned HOL/Real/HahnBanach;
2000-12-06 bauerg 2000-12-06 converted rinv to inverse;
2000-10-23 wenzelm 2000-10-23 intro_classes by default;
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-07 wenzelm 2000-09-07 updated attribute names;
2000-08-17 wenzelm 2000-08-17 renamed 'RS' to 'THEN'; 'symmetric' attribute;
2000-07-23 wenzelm 2000-07-23 classical atts now intro! / intro / intro?;
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-16 wenzelm 2000-07-16 use split_tupled_all;
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-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-02-22 wenzelm 2000-02-22 "cases" method;
2000-02-07 wenzelm 2000-02-07 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
2000-01-28 wenzelm 2000-01-28 eliminated proof script;
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 fixed unfold of facts;
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);