#
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
|