# HG changeset patch # User haftmann # Date 1163428988 -3600 # Node ID 1fd8ba48ae9799a74627bebf9e869224a134214c # Parent 6dd5919e77424f62786722a6c099bad7b85c672a added thy dependencies diff -r 6dd5919e7742 -r 1fd8ba48ae97 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Mon Nov 13 15:43:07 2006 +0100 +++ b/src/HOL/Product_Type.thy Mon Nov 13 15:43:08 2006 +0100 @@ -7,7 +7,7 @@ header {* Cartesian products *} theory Product_Type -imports Fun +imports Typedef Fun Code_Generator uses ("Tools/split_rule.ML") begin