src/HOL/Data_Structures/Define_Time_Function.thy
changeset 80946 b76f64d7d493
parent 80738 6adf6cc82013
child 81088 28ef01901650