src/HOL/Inductive.thy
changeset 45907 4b41967bd77e
parent 45899 df887263a379
child 46008 c296c75f4cf4
     1.1 --- a/src/HOL/Inductive.thy	Sat Dec 17 12:10:37 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Sat Dec 17 12:42:10 2011 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4    ("Tools/inductive.ML")
     1.5    ("Tools/Datatype/datatype_aux.ML")
     1.6    ("Tools/Datatype/datatype_prop.ML")
     1.7 -  ("Tools/Datatype/datatype_abs_proofs.ML")
     1.8    ("Tools/Datatype/datatype_data.ML")
     1.9    ("Tools/Datatype/datatype_case.ML")
    1.10    ("Tools/Datatype/rep_datatype.ML")
    1.11 @@ -277,7 +276,6 @@
    1.12  
    1.13  use "Tools/Datatype/datatype_aux.ML"
    1.14  use "Tools/Datatype/datatype_prop.ML"
    1.15 -use "Tools/Datatype/datatype_abs_proofs.ML"
    1.16  use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    1.17  use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.18  use "Tools/Datatype/rep_datatype.ML"