src/HOL/Analysis/Cross3.thy
changeset 82140 14ab8005f490
parent 81116 0fb1e2dd4122