src/Machine.thy