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.
renamed functor InductFun to Induct;
authorwenzelm
Fri, 24 Jul 2009 12:33:00 +0200
changeset 32171 220abde9962b
parent 32170 541b35729992
child 32172 c4e55f30d527
renamed functor InductFun to Induct;
src/FOL/FOL.thy file | annotate | diff | comparison | revisions
src/HOL/HOL.thy file | annotate | diff | comparison | revisions
src/Tools/induct.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/FOL.thy	Fri Jul 24 12:32:43 2009 +0200
+++ b/src/FOL/FOL.thy	Fri Jul 24 12:33:00 2009 +0200
@@ -360,7 +360,7 @@
 text {* Method setup. *}
 
 ML {*
-  structure Induct = InductFun
+  structure Induct = Induct
   (
     val cases_default = @{thm case_split}
     val atomize = @{thms induct_atomize}
--- a/src/HOL/HOL.thy	Fri Jul 24 12:32:43 2009 +0200
+++ b/src/HOL/HOL.thy	Fri Jul 24 12:33:00 2009 +0200
@@ -1446,7 +1446,7 @@
 text {* Method setup. *}
 
 ML {*
-structure Induct = InductFun
+structure Induct = Induct
 (
   val cases_default = @{thm case_split}
   val atomize = @{thms induct_atomize}
--- a/src/Tools/induct.ML	Fri Jul 24 12:32:43 2009 +0200
+++ b/src/Tools/induct.ML	Fri Jul 24 12:33:00 2009 +0200
@@ -70,7 +70,7 @@
   val setup: theory -> theory
 end;
 
-functor InductFun(Data: INDUCT_DATA): INDUCT =
+functor Induct(Data: INDUCT_DATA): INDUCT =
 struct
isabelle