| Tue, 06 Nov 2001 23:55:19 +0100 | wenzelm | pretty_goals_local: observes context syntax; | changeset | files |
| Tue, 06 Nov 2001 23:54:09 +0100 | wenzelm | defines: Thm.def_name, proper check of args; | changeset | files |
| Tue, 06 Nov 2001 23:53:28 +0100 | wenzelm | separate "in" locale vs. ad-hoc context; | changeset | files |