isabelle: src/HOL/Library/Code_Target_Numeral.thy@bcf2123d059a (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	nipkow
	Wed, 24 Aug 2016 11:02:23 +0200
changeset 63720	bcf2123d059a
parent 60868	dd18c33c001e
child 81713	378b9d6c52b2
permissions	-rw-r--r--