src/HOL/Complex.thy
changeset 74056 fb8d5c0133c9
parent 73928 3b76524f5a85
child 74223 527088d4a89b
equal deleted inserted replaced
74055:0ee44ed80290 74056:fb8d5c0133c9