Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- merged
- Strengthened multiset lemmas w.r.t. irrefl and irreflp
The file was modified | NEWS |
The file was modified | src/HOL/Library/Multiset.thy |
Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)
Summary
- Fixed proofs following Isabelle/a7d2a7a737b8
- added lemmas mem_range_varsI and imgu_subst_domain_subset
- weakened the definition of redundant_inference
The file was modified | thys/Multiset_Ordering_NPC/Multiset_Ordering_More.thy |
The file was modified | thys/Nested_Multisets_Ordinals/McCarthy_91.thy |
The file was modified | thys/Weighted_Path_Order/Multiset_Extension_Pair.thy |
The file was modified | thys/First_Order_Terms/Term.thy |
The file was modified | thys/First_Order_Terms/Unification.thy |
The file was modified | thys/SuperCalc/superposition.thy |