isabelle: src/HOL/Library/Code_Target_Numeral.thy@a7394aa4d21c (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	wenzelm
	Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151	a7394aa4d21c
parent 60868	dd18c33c001e
permissions	-rw-r--r--