isabelle: src/HOL/Library/Code_Target_Numeral.thy@0263787a06b4 (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
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals haftmann parents: diff changeset	8	imports Code_Target_Int Code_Target_Nat
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	paulson <lp15@cam.ac.uk>
	Sat, 04 Dec 2021 20:30:16 +0000
changeset 74878	0263787a06b4
parent 60868	dd18c33c001e
child 81713	378b9d6c52b2
permissions	-rw-r--r--