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")