src/HOL/Complex/ex/MIR.thy
changeset 28540 541366e3c1b3
parent 28290 4cc2b6046258
child 28741 1b257449f804