src/HOL/Library/Realizers.thy
changeset 69605 a96320074298
parent 67319 07176d5b81d5
equal deleted inserted replaced
69604:d80b2df54d31 69605:a96320074298
     6 
     6 
     7 theory Realizers
     7 theory Realizers
     8 imports Main
     8 imports Main
     9 begin
     9 begin
    10 
    10 
    11 ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
    11 ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close>
    12 ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
    12 ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close>
    13 
    13 
    14 end
    14 end