equal
deleted
inserted
replaced
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 |