import FixedPoint instead of Gfp
authoravigad
Wed Aug 03 14:48:13 2005 +0200 (2005-08-03)
changeset 17009932e0e370926
parent 17008 8cb21ca7d480
child 17010 5abc26872268
import FixedPoint instead of Gfp
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Wed Aug 03 14:48:07 2005 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Aug 03 14:48:13 2005 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Support for inductive sets and types *}
     1.5  
     1.6  theory Inductive 
     1.7 -imports Gfp Sum_Type Relation Record
     1.8 +imports FixedPoint Sum_Type Relation Record
     1.9  uses
    1.10    ("Tools/inductive_package.ML")
    1.11    ("Tools/inductive_realizer.ML")