| changeset 29841 | 86d94bb79226 |
| parent 29835 | 62da280e5d0b |
| child 29906 | 80369da39838 |
--- a/src/HOL/Library/Finite_Cartesian_Product.thy Mon Feb 09 16:42:15 2009 +0000 +++ b/src/HOL/Library/Finite_Cartesian_Product.thy Mon Feb 09 16:43:52 2009 +0000 @@ -6,7 +6,8 @@ header {* Definition of finite Cartesian product types. *} theory Finite_Cartesian_Product -imports Plain SetInterval ATP_Linkup + (* imports Plain SetInterval ATP_Linkup *) +imports Main begin (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*)