src/HOL/Complex/ex/linrtac.ML
changeset 27718 3a85bc6bfd73
parent 27436 9581777503e9
child 28290 4cc2b6046258