| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
81b3bbe4 |
|
01-Oct-2016 |
wenzelm <none@none> |
clarified lfp/gfp statements and proofs;
|
| #
32c860d4 |
|
06-Sep-2016 |
wenzelm <none@none> |
clarified proof: save 1-2s CPU time;
|
| #
45a0e905 |
|
05-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
| #
004e4fdf |
|
16-Nov-2015 |
Andreas Lochbihler <none@none> |
export internal definition
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
a9631d56 |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
move some lemmas from AFP/Coinductive
|
| #
b4ae9938 |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
add lemmas
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
eb5ad205 |
|
05-Dec-2013 |
Andreas Lochbihler <none@none> |
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
|
| #
a69c3d9e |
|
02-Sep-2013 |
Andreas Lochbihler <none@none> |
move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
|
| #
d7898d1c |
|
29-Dec-2011 |
huffman <none@none> |
remove constant 'ccpo.lub', re-use constant 'Sup' instead
|
| #
fe7556fe |
|
29-Oct-2010 |
krauss <none@none> |
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
|
| #
05ebef02 |
|
23-Oct-2010 |
krauss <none@none> |
Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem
|