src/HOL/Complex/ex/MIR.thy
changeset 28711 60e51a045755
parent 28290 4cc2b6046258
child 28741 1b257449f804