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