src/HOL/Library/Formal_Power_Series.thy
changeset 30077 c5920259850c
parent 29915 2146e512cec9
child 30273 ecd6f0ca62ea