src/HOL/Data_Structures/Define_Time_0.ML
changeset 80585 9c6cfac291f4
parent 79969 4aeb25ba90f3
equal deleted inserted replaced
80584:b1b53f6a08fa 80585:9c6cfac291f4