| changeset 16417 | 9bc16273c2d4 |
| parent 13783 | 3294f727e20d |
| child 27541 | 9e585e99b494 |
--- a/src/HOL/Algebra/abstract/Abstract.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Algebra/abstract/Abstract.thy Fri Jun 17 16:12:49 2005 +0200 @@ -4,6 +4,6 @@ Author: Clemens Ballarin, started 17 July 1997 *) -theory Abstract = RingHomo + Field: +theory Abstract imports RingHomo Field begin end