src/Doc/Tutorial/Misc/Option2.thy
changeset 58080 42e998248ddc
parent 48985 5386df44a037
child 58860 fee7cfa69c50
equal deleted inserted replaced
58079:df0d6ce8fb66 58080:42e998248ddc