src/HOL/Inductive.thy
changeset 24720 4d2f2e375fa1
parent 24699 c6674504103f
child 24845 abcd15369ffa
--- a/src/HOL/Inductive.thy	Wed Sep 26 11:27:46 2007 +0200
+++ b/src/HOL/Inductive.thy	Wed Sep 26 19:17:55 2007 +0200
@@ -9,8 +9,6 @@
 imports FixedPoint Sum_Type
 uses
   ("Tools/inductive_package.ML")
-  (*("Tools/inductive_set_package.ML")
-  ("Tools/inductive_realizer.ML")*)
   "Tools/dseq.ML"
   ("Tools/inductive_codegen.ML")
   ("Tools/datatype_aux.ML")