src/HOL/Data_Structures/Define_Time_0.ML
changeset 81278 41e843d901ee
parent 79969 4aeb25ba90f3
equal deleted inserted replaced
81277:0eb96012d416 81278:41e843d901ee