History log of /seL4-l4v-master/isabelle/src/HOL/ex/Code_Binary_Nat_examples.thy
Revision Date Author Comments
# 17bc899d 18-Aug-2017 wenzelm <none@none>

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
# ee8e8234 06-Oct-2015 wenzelm <none@none>

isabelle update_cartouches;
# 794edf80 02-Nov-2014 wenzelm <none@none>

modernized header uniformly as section;
# 5a8927d0 15-Feb-2013 haftmann <none@none>

two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one

--HG--
extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
# 8375a521 08-Nov-2012 haftmann <none@none>

refined stack of library theories implementing int and/or nat by target language numerals

--HG--
rename : src/HOL/Library/Code_Nat.thy => src/HOL/Library/Code_Binary_Nat.thy
rename : src/HOL/ex/Code_Nat_examples.thy => src/HOL/ex/Code_Binary_Nat_examples.thy