| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
e1f0bba9 |
|
11-Sep-2014 |
blanchet <none@none> |
fixed some spelling mistakes
|
| #
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
| #
40e0ba91 |
|
12-Feb-2014 |
blanchet <none@none> |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
a6c1110f |
|
12-Feb-2014 |
blanchet <none@none> |
adapted theories to '{case,rec}_{list,option}' names
|
| #
7b569724 |
|
07-Jul-2013 |
wenzelm <none@none> |
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
--HG--
rename : src/Doc/HOL/document/HOL.tex => src/Doc/Logics/document/HOL.tex
|