Skip to content
Success

Changes

Summary

  1. proper logical constants
  2. prefer existing logical constant over abbreviation
  3. dropped aliasses
  4. remove potentially dangerous simp rule prime_dvd_mult_iff
Changeset 7521:c86adbf1663e by haftmann:
proper logical constants
The file was modified thys/Coinductive/Coinductive_List.thy (diff)
The file was modified thys/Containers/Set_Linorder.thy (diff)
The file was modified thys/JinjaThreads/Common/SemiType.thy (diff)
The file was modified thys/JinjaThreads/Common/WellForm.thy (diff)
The file was modified thys/JinjaThreads/MM/JMM_Spec.thy (diff)
The file was modified thys/JinjaThreads/MM/Orders.thy (diff)
The file was modified thys/Lambda_Free_RPOs/Extension_Orders.thy (diff)
The file was modified thys/Lambda_Free_RPOs/Lambda_Free_Util.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Nested_Multiset.thy (diff)
The file was modified thys/Refine_Monadic/examples/WordRefine.thy (diff)
Changeset 7520:06b76b5913f2 by haftmann:
prefer existing logical constant over abbreviation
The file was modified thys/Coinductive/Coinductive_List.thy (diff)
The file was modified thys/JinjaThreads/MM/JMM_Spec.thy (diff)
The file was modified thys/JinjaThreads/MM/Orders.thy (diff)
The file was modified thys/List-Infinite/CommonSet/SetInterval2.thy (diff)
The file was modified thys/Stable_Matching/Basis.thy (diff)
The file was modified thys/SuperCalc/superposition.thy (diff)
Changeset 7519:02dfc56df9bc by haftmann:
dropped aliasses
The file was modified thys/Free-Groups/Cancelation.thy (diff)
The file was modified thys/Free-Groups/FreeGroups.thy (diff)
The file was modified thys/JinjaThreads/MM/Orders.thy (diff)
The file was modified thys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy (diff)
Changeset 7518:79d2990585f0 by haftmann:
remove potentially dangerous simp rule prime_dvd_mult_iff
The file was modified thys/Algebraic_Numbers/Algebraic_Numbers.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy (diff)
The file was modified thys/Coinductive/Examples/Hamming_Stream.thy (diff)
The file was modified thys/Fermat3_4/Fermat3.thy (diff)
The file was modified thys/Fermat3_4/Quad_Form.thy (diff)
The file was modified thys/Polynomial_Factorization/Gauss_Lemma.thy (diff)
The file was modified thys/RSAPSS/Productdivides.thy (diff)
The file was modified thys/SumSquares/FourSquares.thy (diff)
The file was modified thys/SumSquares/TwoSquares.thy (diff)