| changeset 16417 | 9bc16273c2d4 |
| parent 15172 | 73069e033a0b |
| child 18460 | 9a1458cb2956 |
--- a/src/HOL/Induct/QuoDataType.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,7 +7,7 @@ header{*Defining an Initial Algebra by Quotienting a Free Algebra*} -theory QuoDataType = Main: +theory QuoDataType imports Main begin subsection{*Defining the Free Algebra*}