src/HOL/Library/Open_State_Syntax.thy
changeset 72036 e48a5b6b7554
parent 69593 3dda49e08b9d
child 72581 de581f98a3a1