src/HOL/Library/Open_State_Syntax.thy
changeset 71588 f3fe59e61f3d
parent 69593 3dda49e08b9d
child 72581 de581f98a3a1