| changeset 15131 | c69542757a4d |
| parent 14952 | 47455995693d |
| child 15140 | 322485b816ac |
--- a/src/HOL/Product_Type.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Product_Type.thy Mon Aug 16 14:22:27 2004 +0200 @@ -6,8 +6,10 @@ header {* Cartesian products *} -theory Product_Type = Fun -files ("Tools/split_rule.ML"): +theory Product_Type +import Fun +files ("Tools/split_rule.ML") +begin subsection {* Unit *}