History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Library/Nat_Bijection.thy
Revision Date Author Comments
# a4bab154 04-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# a7ccdf43 10-Jan-2018 nipkow <none@none>

ran isabelle update_op on all sources


# 351cc2e6 17-Oct-2016 nipkow <none@none>

setsum -> sum


# 24c52962 06-Aug-2016 wenzelm <none@none>

misc tuning and modernization;


# db83087d 03-Jan-2016 wenzelm <none@none>

tuned whitespace;


# a0af5cdd 17-Jun-2015 wenzelm <none@none>

isabelle update_cartouches;


# f2ba2c03 01-Jun-2015 haftmann <none@none>

separate class for division operator, with particular syntax added in more specific classes


# 8f7c4718 10-Feb-2015 paulson <lp15@cam.ac.uk>

Not a simprule, as it complicates proofs


# 34a3534a 02-Nov-2014 wenzelm <none@none>

modernized header;


# dc5a029e 30-Oct-2014 haftmann <none@none>

more simp rules concerning dvd and even/odd

--HG--
extra : rebase_source : 895ed3f871c22790e8d199a30828e91bc13bd735


# 06e59c9f 23-Oct-2014 haftmann <none@none>

downshift of theory Parity in the hierarchy


# 830e17f5 19-Oct-2014 haftmann <none@none>

augmented and tuned facts on even/odd and division


# e46c07fd 04-Jul-2014 haftmann <none@none>

reduced name variants for assoc and commute on plus and mult


# d4cae3bf 23-Mar-2013 haftmann <none@none>

fundamental revision of big operators on sets


# 11c94dbe 13-Mar-2013 paulson <none@none>

new lemma subset_decode_imp_le


# 6b0b29ec 13-Mar-2011 wenzelm <none@none>

tuned headers;


# 5b59da77 13-Sep-2010 nipkow <none@none>

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI


# 68b10498 28-Jun-2010 haftmann <none@none>

merged constants "split" and "prod_case"


# 1aada616 10-Mar-2010 huffman <none@none>

new theory Library/Nat_Bijection.thy