src/HOL/Data_Structures/Define_Time_Function.thy
changeset 80340 992bd899a027
parent 79973 7bbb0d65ce72
child 80738 6adf6cc82013
equal deleted inserted replaced
80339:7b948ca986ec 80340:992bd899a027