Summary
- "tl" is part of "generate"; replaced "in_" lemmas (what properties do elements of certain set satisfy) by "set_" lemmas (explicit equations to set comprehension)
- merged
- simplified definition
- tuned op's
The file was modified | thys/Diophantine_Eqns_Lin_Hom/Algorithm.thy (diff) |
The file was modified | thys/Diophantine_Eqns_Lin_Hom/Algorithm.thy (diff) |
The file was modified | thys/Modal_Logics_for_NTS/FS_Set.thy (diff) |
The file was modified | thys/Nested_Multisets_Ordinals/Signed_Multiset.thy (diff) |