Skip to content
Failed

Changes

Summary

  1. "tl" is part of "generate"; replaced "in_" lemmas (what properties do elements of certain set satisfy) by "set_" lemmas (explicit equations to set comprehension)
  2. merged
  3. simplified definition
  4. tuned op's
Changeset 8678:697ddf9eec0d by Christian Sternagel:
"tl" is part of "generate"; replaced "in_" lemmas (what properties do elements of certain set satisfy) by "set_" lemmas (explicit equations to set comprehension)
The file was modified thys/Diophantine_Eqns_Lin_Hom/Algorithm.thy (diff)
Changeset 8677:9fa403e6eec1 by Christian Sternagel:
merged
Changeset 8676:4738759e8529 by Christian Sternagel:
simplified definition
The file was modified thys/Diophantine_Eqns_Lin_Hom/Algorithm.thy (diff)
Changeset 8675:8d43954c96fd by nipkow:
tuned op's
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)