src/HOL/Inductive.thy
changeset 48357 828ace4f75ab
parent 46950 d0181abdbdac
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Inductive.thy	Thu Jul 19 12:01:05 2012 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Jul 19 19:38:39 2012 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    "rep_datatype" :: thy_goal and
     1.5    "primrec" :: thy_decl
     1.6  uses
     1.7 -  "Tools/dseq.ML"
     1.8    ("Tools/inductive.ML")
     1.9    ("Tools/Datatype/datatype_aux.ML")
    1.10    ("Tools/Datatype/datatype_prop.ML")