Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
import FixedPoint instead of Gfp
authoravigad
Wed, 03 Aug 2005 14:48:13 +0200
changeset 17009 932e0e370926
parent 17008 8cb21ca7d480
child 17010 5abc26872268
import FixedPoint instead of Gfp
src/HOL/Inductive.thy file | annotate | diff | comparison | revisions 
--- 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")
isabelle