isabelle: src/HOL/Library/Code_Target_Numeral.thy@5d0d35680311 (annotated)

50023 28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	1	(* Title: HOL/Library/Code_Target_Numeral.thy
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	2	Author: Florian Haftmann, TU Muenchen
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	3	*)
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	4
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	5	section \<open>Implementation of natural and integer numbers by target-language integers\<close>
50023 28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	6
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	7	theory Code_Target_Numeral
82445 bb1f2a03b370 incorporate target-language integer implementation of bit shifts into Main haftmann parents: 81713 diff changeset	8	imports Code_Target_Nat Code_Target_Int
50023 28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	9	begin
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	10
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	11	end

author	nipkow
	Wed, 25 Jun 2025 14:16:30 +0200
changeset 82735	5d0d35680311
parent 82445	bb1f2a03b370
permissions	-rw-r--r--