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