src/ZF/add_ind_def.ML
changeset 1418 f5f97ee67cbb
parent 1109 380e9eb40db7
child 1461 6bcb44e4d6e5
equal deleted inserted replaced
1417:c0f6a1887518 1418:f5f97ee67cbb
    58   val case_inr	: thm			(*inr equality rule for case*)
    58   val case_inr	: thm			(*inr equality rule for case*)
    59   val inl_iff	: thm			(*injectivity of inl, using <->*)
    59   val inl_iff	: thm			(*injectivity of inl, using <->*)
    60   val inr_iff	: thm			(*injectivity of inr, using <->*)
    60   val inr_iff	: thm			(*injectivity of inr, using <->*)
    61   val distinct	: thm			(*distinctness of inl, inr using <->*)
    61   val distinct	: thm			(*distinctness of inl, inr using <->*)
    62   val distinct'	: thm			(*distinctness of inr, inl using <->*)
    62   val distinct'	: thm			(*distinctness of inr, inl using <->*)
       
    63   val free_SEs  : thm list		(*elim rules for SU, and pair_iff!*)
    63   end;
    64   end;
    64 
    65 
    65 signature ADD_INDUCTIVE_DEF =
    66 signature ADD_INDUCTIVE_DEF =
    66   sig 
    67   sig 
    67   val add_fp_def_i : term list * term * term list -> theory -> theory
    68   val add_fp_def_i : term list * term * term list -> theory -> theory