src/FOLP/classical.ML
changeset 15570 8d8c70b41bab
parent 4653 d60f76680bf4
child 17496 26535df536ae
equal deleted inserted replaced
15569:1b3115d1a8df 15570:8d8c70b41bab
   110   map (pair true) (elims @ swapify intrs)  @  map (pair false) intrs;
   110   map (pair true) (elims @ swapify intrs)  @  map (pair false) intrs;
   111 
   111 
   112 (*Note that allE precedes exI in haz_brls*)
   112 (*Note that allE precedes exI in haz_brls*)
   113 fun make_cs {safeIs,safeEs,hazIs,hazEs} =
   113 fun make_cs {safeIs,safeEs,hazIs,hazEs} =
   114   let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
   114   let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
   115           partition (apl(0,op=) o subgoals_of_brl) 
   115           List.partition (apl(0,op=) o subgoals_of_brl) 
   116              (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
   116              (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
   117   in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
   117   in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
   118         safe0_brls=safe0_brls, safep_brls=safep_brls,
   118         safe0_brls=safe0_brls, safep_brls=safep_brls,
   119         haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))}
   119         haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))}
   120   end;
   120   end;