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.
Legacy ML bindings now refer to old inductive definition package.
authorberghofe
Fri, 13 Oct 2006 18:14:12 +0200
changeset 21019 650c48711c7b
parent 21018 e6b8d6784792
child 21020 9af9ceb16d58
Legacy ML bindings now refer to old inductive definition package.
src/HOL/Finite_Set.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite_Set.ML	Fri Oct 13 18:12:58 2006 +0200
+++ b/src/HOL/Finite_Set.ML	Fri Oct 13 18:14:12 2006 +0200
@@ -7,7 +7,7 @@
   val elims = thms "Finites.cases";
   val elim = thm "Finites.cases";
   val induct = thm "Finites.induct";
-  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
+  val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
   val [emptyI, insertI] = thms "Finites.intros";
 end;
 
@@ -17,7 +17,7 @@
   val elims = thms "foldSet.cases";
   val elim = thm "foldSet.cases";
   val induct = thm "foldSet.induct";
-  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
+  val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
   val [emptyI, insertI] = thms "foldSet.intros";
 end;
isabelle