src/HOL/Complex/ex/linrtac.ML
changeset 28667 4adfdd666e7d
parent 28290 4cc2b6046258
equal deleted inserted replaced
28666:d2dbfe3a0284 28667:4adfdd666e7d