Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move first_countable_topology to the HOL image
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move metric_space to its own theory
Fri, 22 Mar 2013 10:41:42 +0100 hoelzl move topological_space to its own theory
Thu, 21 Mar 2013 16:58:14 +0100 wenzelm proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
Thu, 21 Mar 2013 16:35:53 +0100 wenzelm eliminated char_width_int to avoid unclear rounding;
Thu, 21 Mar 2013 10:05:03 +0100 nipkow proofs depend only on constraints, not on def of L WHILE
Wed, 20 Mar 2013 15:35:35 +0100 blanchet use the right role for SPASS hypotheses
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip