equal
deleted
inserted
replaced
202 \item[\<open>Code_Target_Nat\<close>] implements type \<^typ>\<open>nat\<close> |
202 \item[\<open>Code_Target_Nat\<close>] implements type \<^typ>\<open>nat\<close> |
203 by \<^typ>\<open>integer\<close> and thus by target-language built-in integers. |
203 by \<^typ>\<open>integer\<close> and thus by target-language built-in integers. |
204 Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated |
204 Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated |
205 by a preprocessor. |
205 by a preprocessor. |
206 |
206 |
207 \item[\<open>Code_Target_Bit_Shifts\<close>] implements bit shifts on \<^typ>\<open>integer\<close> |
|
208 by target-language operations. Combined with \<open>Code_Target_Int\<close> |
|
209 or \<open>Code_Target_Nat\<close>, bit shifts on \<^typ>\<open>int\<close> or \<^type>\<open>nat\<close> can |
|
210 be implemented by target-language operations. |
|
211 |
|
212 \item[\<open>Code_Target_Numeral\<close>] is a convenience theory |
207 \item[\<open>Code_Target_Numeral\<close>] is a convenience theory |
213 containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>- |
208 containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>- |
214 |
209 |
215 \item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language |
210 \item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language |
216 integers, sacrificing pattern patching in exchange for dramatically |
211 integers, sacrificing pattern patching in exchange for dramatically |