src/HOL/Reflection/ROOT.ML
changeset 29791 2029482e8942
child 29805 a5da150bd0ab
equal deleted inserted replaced
29790:02557b98bd0a 29791:2029482e8942
       
     1 
       
     2 use_thys ["Cooper", "Ferrack", "MIR"];