1structure optionSimps :> optionSimps = 2struct 3 4open simpLib optionTheory 5 6val OPTION_ss = BasicProvers.thy_ssfrag "option" 7 8end; 9