1structure sumSimps :> sumSimps = 2struct 3 4open sumTheory; 5 6(* Note: OUTL (INR x) is not defined *) 7val compute_thms = 8 [ ISL,ISR,OUTL,OUTR, 9 sum_distinct,Conv.GSYM sum_distinct,INR_INL_11,sum_case_def]; 10 11val SUM_ss = BasicProvers.thy_ssfrag "sum" 12 13val SUM_rws = 14 computeLib.add_thms (List.map computeLib.lazyfy_thm compute_thms); 15 16end (* struct *) 17