src/HOL/Statespace/state_fun.ML
changeset 50808 1702ed63c2db
parent 46218 ecf6375e2abb
child 51717 9e7d1c139569