# HG changeset patch
# User avigad
# Date 1123073293 -7200
# Node ID 932e0e370926de9d8f4ed1f8e672bb880e9dc5bb
# Parent  8cb21ca7d480f2b67b2d4785f9887cd900816abc
import FixedPoint instead of Gfp

diff -r 8cb21ca7d480 -r 932e0e370926 src/HOL/Inductive.thy
--- 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")