src/HOL/Real/HahnBanach/Aux.thy
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-09 bauerg 2000-08-09 tuned;
2000-08-03 wenzelm 2000-08-03 tuned;
2000-07-23 wenzelm 2000-07-23 classical atts now intro! / intro / intro?;
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 completed TYPES version of HahnBanach;
2000-06-07 paulson 2000-06-07 First round of changes, towards installation of simprocs * replacing 0r by (0::real0 * better rewriting, especially pulling out signs in (-x)*y = - (x*y), etc.
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-08 wenzelm 2000-05-08 replaced rabs by overloaded abs;
2000-02-07 wenzelm 2000-02-07 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
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);