equal
deleted
inserted
replaced
76 apply (rule Inl_Rep_not_Inr_Rep) |
76 apply (rule Inl_Rep_not_Inr_Rep) |
77 apply (rule Inl_RepI) |
77 apply (rule Inl_RepI) |
78 apply (rule Inr_RepI) |
78 apply (rule Inr_RepI) |
79 done |
79 done |
80 |
80 |
81 lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard, iff] |
81 lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard] |
|
82 declare Inr_not_Inl [iff] |
82 |
83 |
83 lemmas Inl_neq_Inr = Inl_not_Inr [THEN notE, standard] |
84 lemmas Inl_neq_Inr = Inl_not_Inr [THEN notE, standard] |
84 lemmas Inr_neq_Inl = sym [THEN Inl_neq_Inr, standard] |
85 lemmas Inr_neq_Inl = sym [THEN Inl_neq_Inr, standard] |
85 |
86 |
86 |
87 |