| #
5fccd0bf |
|
08-Oct-2019 |
haftmann <none@none> |
formally augmented corresponding rules for field_simps
--HG--
extra : rebase_source : 10a72e1ed5967c95cb98493db93fec6c7d0f8230
|
| #
075e0a05 |
|
01-Apr-2019 |
paulson <lp15@cam.ac.uk> |
A few results in Algebra, and bits for Analysis
|
| #
ab32308e |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
renamings and new material
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
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.
|
| #
0f360eed |
|
13-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying
|
| #
9e94ca85 |
|
12-Jul-2018 |
immler <none@none> |
relaxed assumptions for dim_image_eq and dim_image_le
|
| #
a9b271d6 |
|
11-Jun-2018 |
immler <none@none> |
default value for parametricity of dim
|
| #
dcc6865b |
|
06-Jun-2018 |
wenzelm <none@none> |
isabelle update_comments;
|
| #
6437a27a |
|
15-May-2018 |
wenzelm <none@none> |
tuned headers;
|
| #
f4f1a444 |
|
15-May-2018 |
immler <none@none> |
move FuncSet back to HOL-Library (amending 493b818e8e10)
--HG--
rename : src/HOL/FuncSet.thy => src/HOL/Library/FuncSet.thy
|
| #
b3832654 |
|
03-May-2018 |
immler <none@none> |
fixed HOL-Analysis
|
| #
e04b7748 |
|
02-May-2018 |
immler <none@none> |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
--HG--
rename : src/HOL/Library/FuncSet.thy => src/HOL/FuncSet.thy
|