| #
d4b0f203 |
|
20-Apr-2019 |
haftmann <none@none> |
clarified notation
|
| #
61afea2c |
|
01-Sep-2016 |
wenzelm <none@none> |
clarified session;
misc tuning and modernization;
--HG--
rename : src/HOL/Word/Type_Length.thy => src/HOL/Library/Type_Length.thy
|
| #
c7eae65a |
|
11-Jul-2016 |
wenzelm <none@none> |
tuned;
|
| #
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
| #
8e8b881c |
|
04-Nov-2015 |
ballarin <none@none> |
Keyword 'rewrites' identifies rewrite morphisms.
|
| #
44916bcd |
|
24-Sep-2015 |
wenzelm <none@none> |
explicit indication of overloaded typedefs;
|
| #
94ea3a82 |
|
06-Jul-2015 |
wenzelm <none@none> |
tuned proofs;
|
| #
a0af5cdd |
|
17-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
fcdfcd00 |
|
11-Apr-2015 |
wenzelm <none@none> |
tuned;
|
| #
34a3534a |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
ac866a0f |
|
25-Dec-2013 |
haftmann <none@none> |
prefer more canonical names for lemmas on min/max
|
| #
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
| #
de37771f |
|
26-Mar-2013 |
haftmann <none@none> |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
| #
aabb89b5 |
|
26-Mar-2013 |
wenzelm <none@none> |
tuned imports;
|
| #
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
| #
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
| #
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
| #
c57f60d9 |
|
27-Dec-2011 |
haftmann <none@none> |
be explicit about Finite_Set.fold
|
| #
91e6e1da |
|
30-Nov-2011 |
wenzelm <none@none> |
tuned header;
|
| #
ee79c61b |
|
11-Sep-2011 |
huffman <none@none> |
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
|
| #
e987d1be |
|
08-Sep-2011 |
huffman <none@none> |
Library/Saturated.thy: number_semiring class instance
|
| #
378675b3 |
|
08-Sep-2011 |
huffman <none@none> |
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
|
| #
45b17abb |
|
07-Sep-2011 |
haftmann <none@none> |
theory of saturated naturals contributed by Peter Gammie
|