author | wenzelm |
Wed, 26 Sep 2007 19:17:55 +0200 | |
changeset 24720 | 4d2f2e375fa1 |
parent 24719 | 21d1cdab2d8c |
child 24721 | 2a029b78db60 |
--- 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")