src/HOL/Data_Structures/Define_Time_Function.ML
changeset 81184 f270cd6ee185
parent 81147 503e5280ba72
child 81255 47530e9a7c33
equal deleted inserted replaced
81183:10e3a30b2512 81184:f270cd6ee185