src/HOL/Probability/Sinc_Integral.thy
changeset 80611 fbc859ccdaf3
parent 80175 200107cdd3ac
child 82538 4b132ea7d575