src/HOL/Complex/ex/linrtac.ML
changeset 23719 ccd9cb15c062
parent 23590 ad95084a5c63
child 26075 815f3ccc0b45