src/Doc/Tutorial/Misc/Option2.thy
changeset 59143 15c342a9a8e0
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
59142:705f8aea8d60 59143:15c342a9a8e0