src/1/ConseqConv.sml

542      val (n1, thm1) = check_sys_call sys [] context 0 dir b1;
545      (n1, thm2)
566      val (n1, thm1) = check_sys_call sys [] context 0  (CONSEQ_CONV_DIRECTION_NEGATE dir) b1;
571      (n1, thm3)
598      val (n1, thm1_opt) = sys [b2] context 0  dir b1;
600      val (n2, thm2_opt) = sys [a2] context n1 dir b2;
622      val (n1, thm1_opt) = sys [] context 0  dir b1;
625      val (n2, thm2_opt) = if abort_cond then (n1, NONE) else sys [] context n1 dir b2;
662      val (n1, thm1_opt) = sys [a1] context 0  dir b1;
664      val (n2, thm2_opt) = sys [a2] context n1 dir b2;
685      val (n1, thm1_opt) = sys [] context 0  dir b1;
688      val (n2, thm2_opt) = if abort_cond then (n1, NONE) else sys [] context n1 dir b2;
726      val (n1, thm1_opt) = sys [a1] context 0 dir b2;
728      val (n2, thm2_opt) = sys [a2] context n1 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1;
749      val (n1, thm1_opt) = sys [] context 0 dir b2;
752      val (n2, thm2_opt) = if abort_cond then (n1, NONE) else sys [] context n1 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1;
769      val (n1, thm1_opt) = sys [] context 0 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1;
772      val (n2, thm2_opt) = if abort_cond then (n1, NONE) else
773             sys [a2] context n1 dir b2;
815      val (n1, thm1_opt) = sys [] context 0  dir b1;
816      val (n2, thm2_opt) = sys [] context n1 dir b2;
832      val (n1, thm1_opt) = sys [c] context 0  dir b1;
833      val (n2, thm2_opt) = sys [mk_neg c] context n1 dir b2;
859      val (n1, thm1_opt) = sys [] (var_filter_context v context) 0 dir b1;
865      (n1, thm3)
872      val (n1, thm1_opt) = sys [] (var_filter_context v context) 0 dir b1;
878      (n1, thm3)
1172      val (congs_flag, n1, thm1_opt) = if isSome result_opt then
1177      val (n2, thm2_opt) = if not do_depth_call then (n1, thm1_opt) else
1183                      redepth context n1 step_opt congs_flag dir t2