changeset 17009 | 932e0e370926 |
parent 16417 | 9bc16273c2d4 |
child 18456 | 8cc35e95450a |
--- a/src/HOL/Inductive.thy Wed Aug 03 14:48:07 2005 +0200 +++ b/src/HOL/Inductive.thy Wed Aug 03 14:48:13 2005 +0200 @@ -6,7 +6,7 @@ header {* Support for inductive sets and types *} theory Inductive -imports Gfp Sum_Type Relation Record +imports FixedPoint Sum_Type Relation Record uses ("Tools/inductive_package.ML") ("Tools/inductive_realizer.ML")