# [isabelle] HOL-Word contains trivial lemmas

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] HOL-Word contains trivial lemmas
*From*: Lars Hupel <hupel at in.tum.de>
*Date*: Thu, 16 Apr 2015 17:36:52 +0200
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

It appears that there are two occurrences of "True" in HOL-Word:
lemma "True"
Auto solve_direct: The current goal can be solved directly with
HOL.TrueI: True
Word_Miscellaneous.z1pdiv2': True
Word_Miscellaneous.z1pmod2': True
The definitions of these lemmas are:
lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]
lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]
This is already the case for Isabelle2014.
I guess the header of the Word_Miscellaneous theory is even more spot on
than Florian intended :-)
header {* Miscellaneous lemmas, of at least doubtful value *}
Cheers
Lars

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*