src/HOL/Tools/Nitpick/nitpick_peephole.ML
changeset 34936 c4f04bee79f3
parent 34126 8a2c5d7aff51
child 34982 7b8c366e34a2
equal deleted inserted replaced
34935:cb011ba38950 34936:c4f04bee79f3
   419         s_and (s_subset r11 r2) (s_subset r12 r2)
   419         s_and (s_subset r11 r2) (s_subset r12 r2)
   420       | s_subset r1 (r2 as Union (r21, r22)) =
   420       | s_subset r1 (r2 as Union (r21, r22)) =
   421         if is_one_rel_expr r1 then
   421         if is_one_rel_expr r1 then
   422           s_or (s_subset r1 r21) (s_subset r1 r22)
   422           s_or (s_subset r1 r21) (s_subset r1 r22)
   423         else
   423         else
   424           if s_subset r1 r21 = True orelse s_subset r1 r22 = True
   424           if s_subset r1 r21 = True orelse s_subset r1 r22 = True orelse
   425              orelse r1 = r2 then
   425              r1 = r2 then
   426             True
   426             True
   427           else
   427           else
   428             Subset (r1, r2)
   428             Subset (r1, r2)
   429       | s_subset r1 r2 =
   429       | s_subset r1 r2 =
   430         if r1 = r2 orelse is_none_product r1 then True
   430         if r1 = r2 orelse is_none_product r1 then True