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