equal
deleted
inserted
replaced
126 shows "pders_Set UNIV1 ONE = {}" |
126 shows "pders_Set UNIV1 ONE = {}" |
127 unfolding UNIV1_def pders_Set_def by (auto split: if_splits) |
127 unfolding UNIV1_def pders_Set_def by (auto split: if_splits) |
128 |
128 |
129 lemma pders_Set_CHAR [simp]: |
129 lemma pders_Set_CHAR [simp]: |
130 shows "pders_Set UNIV1 (CHAR c) = {ONE}" |
130 shows "pders_Set UNIV1 (CHAR c) = {ONE}" |
131 unfolding UNIV1_def pders_Set_def |
131 unfolding UNIV1_def pders_Set_def |
132 apply(auto) |
132 apply(auto) |
133 apply(frule rev_subsetD) |
133 apply(frule rev_subsetD) |
134 apply(rule pders_CHAR) |
134 apply(rule pders_CHAR) |
135 apply(simp) |
135 apply(simp) |
136 apply(case_tac xa) |
136 apply(case_tac xa) |