History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Modules.thy
Revision Date Author Comments
# a4784f6f 09-Oct-2019 haftmann <none@none>

dedicated fact collections for algebraic simplification rules potentially splitting goals

--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
# 5fccd0bf 08-Oct-2019 haftmann <none@none>

formally augmented corresponding rules for field_simps

--HG--
extra : rebase_source : 10a72e1ed5967c95cb98493db93fec6c7d0f8230
# 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.
# 6437a27a 15-May-2018 wenzelm <none@none>

tuned headers;
# 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