src/Provers/clasimp.ML
changeset 18448 6e805f389355
parent 17879 88844eea4ce2
child 18529 540da2415751
equal deleted inserted replaced
18447:da548623916a 18448:6e805f389355
   139     val (elim, intro) = if n = 0 then decls1 else decls2;
   139     val (elim, intro) = if n = 0 then decls1 else decls2;
   140     val zero_rotate = zero_var_indexes o rotate_prems n;
   140     val zero_rotate = zero_var_indexes o rotate_prems n;
   141   in
   141   in
   142     (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
   142     (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
   143            [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
   143            [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
   144       handle THM _ => (elim (cs, [suffix_thm name "_iff" (zero_rotate (th RS Data.notE))])
   144       handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
   145         handle THM _ => intro (cs, [th])),
   145         handle THM _ => intro (cs, [th])),
   146      simp (ss, [th]))
   146      simp (ss, [th]))
   147   end;
   147   end;
   148 
   148 
   149 fun delIff delcs delss ((cs, ss), th) =
   149 fun delIff delcs delss ((cs, ss), th) =