| #
39fbc3fd |
|
18-Jan-2019 |
immler <none@none> |
restore type variable names in unoverload_type
--HG--
extra : rebase_source : 5bebe9c7a6774e498f5c496fcd7ff8b9b932efb0
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
23ca233b |
|
14-Nov-2018 |
immler <none@none> |
extract example for ab_group_add_on_with
|
| #
8fc0aae3 |
|
14-Nov-2018 |
immler <none@none> |
generalized local_typedef_ab_group_add
|
| #
91370a94 |
|
13-Nov-2018 |
immler <none@none> |
use locales in Group_On_With
|
| #
dbf3acf7 |
|
29-Sep-2018 |
immler <none@none> |
fix (non-existent) document generation
|
| #
cc37beb1 |
|
24-Sep-2018 |
nipkow <none@none> |
Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.
|
| #
9e94ca85 |
|
12-Jul-2018 |
immler <none@none> |
relaxed assumptions for dim_image_eq and dim_image_le
|
| #
517c8ccd |
|
28-Jun-2018 |
immler <none@none> |
transfer more lemmas
|
| #
8c1b61fc |
|
28-Jun-2018 |
immler <none@none> |
fixed some oversights
|
| #
13666d4b |
|
28-Jun-2018 |
immler <none@none> |
avoid duplicate facts, the "trick" was copied without deeper motivation
--HG--
extra : rebase_source : b16f4c46fb82fdffffb4b79e6e7acc46bb82e0ef
|
| #
5c6f3ded |
|
27-Jun-2018 |
immler <none@none> |
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
|