src/HOL/Analysis/Abstract_Euclidean_Space.thy
changeset 82338 1eb12389c499
parent 82323 b022c013b04b
equal deleted inserted replaced
82337:3ae491533076 82338:1eb12389c499