src/HOL/Library/Old_Datatype.thy
changeset 67319 07176d5b81d5
parent 67318 0ee38196509e
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:11:20 2018 +0100
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:17:13 2018 +0100
     1.3 @@ -9,9 +9,6 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
     1.8 -ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
     1.9 -
    1.10  
    1.11  subsection \<open>The datatype universe\<close>
    1.12