src/HOL/Statespace/StateFun.thy
changeset 26715 00ff79ab6e6b
parent 25408 156f6f7082b8
child 35114 b1fd1d756e20