Lines Matching defs:nl
2769 val nl = get_resort_list___pred is_asl_star sfb;
2771 if null nl then get_resort_thm L else
2772 (c (BAG_RESORT_CONV nl) tt, thm)
2801 val nl = get_resort_list___pred is_asl_trivial_cond sfb;
2803 if null nl then get_resort_thm L else
2804 (c (BAG_RESORT_CONV nl) tt, thm, has_precond)
2831 val nl = get_resort_list___pred is_asl_false sfb;
2833 if null nl then get_resort_thm L else
2834 (c (BAG_RESORT_CONV nl) tt, thm)
2855 val nl = get_resort_list___pred is_asl_exists sfb;
2857 if null nl then get_resort_thm L else
2858 (c (BAG_RESORT_CONV nl) tt, thm)