equal
deleted
inserted
replaced
178 lemma card_UNIV_char: |
178 lemma card_UNIV_char: |
179 "card (UNIV :: char set) = 256" |
179 "card (UNIV :: char set) = 256" |
180 by (auto simp add: UNIV_char_of_nat card_image) |
180 by (auto simp add: UNIV_char_of_nat card_image) |
181 |
181 |
182 context |
182 context |
183 includes lifting_syntax integer.lifting natural.lifting |
183 includes lifting_syntax and integer.lifting and natural.lifting |
184 begin |
184 begin |
185 |
185 |
186 lemma [transfer_rule]: |
186 lemma [transfer_rule]: |
187 \<open>(pcr_integer ===> (=)) char_of char_of\<close> |
187 \<open>(pcr_integer ===> (=)) char_of char_of\<close> |
188 by (unfold char_of_def) transfer_prover |
188 by (unfold char_of_def) transfer_prover |