src/HOL/Statespace/state_fun.ML
changeset 39564 acfd10e38e80
parent 39159 0dec18004e75
child 41227 11e7ee2ca77f