| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
f67d856d |
|
25-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
19e3dfe6 |
|
06-Apr-2012 |
haftmann <none@none> |
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
|
| #
99b811bf |
|
23-Jan-2012 |
huffman <none@none> |
generalize type of List.listrel
|
| #
c67e1024 |
|
06-Jan-2012 |
haftmann <none@none> |
tuned proofs
--HG--
extra : rebase_source : 43faf05606d15d9a4206932929e120f35273e22b
|
| #
d592392c |
|
24-Dec-2011 |
haftmann <none@none> |
tuned proofs
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
a85418b7 |
|
29-Sep-2010 |
haftmann <none@none> |
fact listsum now names listsum_foldl
|
| #
a9cb65ea |
|
22-Sep-2010 |
nipkow <none@none> |
more lists lemmas
|
| #
0264597a |
|
16-Sep-2010 |
paulson <none@none> |
tidied a few proofs
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
1ff366c9 |
|
13-Dec-2008 |
berghofe <none@none> |
Modified nominal_primrec to make it work with local theories, unified syntax
with the one used by fun(ction) and new version of primrec command.
|
| #
d79d3e16 |
|
16-Jul-2008 |
berghofe <none@none> |
Added Standardization theory.
|