src/HOL/Library/Formal_Power_Series.thy
changeset 30202 2775062fd3a9
parent 29915 2146e512cec9
child 30273 ecd6f0ca62ea