src/HOL/Library/Open_State_Syntax.thy
changeset 68860 f443ec10447d
parent 68224 1f7308050349
child 69593 3dda49e08b9d