Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. prefer [simp] over [iff] as [iff] break HOL-UNITY
  3. fix LaTeX error
  4. add lemmas contributed by Peter Gammie
Changeset 63564:eca71be9c948 by Andreas Lochbihler:
merged
Changeset 63563:0bcd79da075b by Andreas Lochbihler:
prefer [simp] over [iff] as [iff] break HOL-UNITY
The file was modified src/HOL/Order_Relation.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 63562:6f7a9d48a828 by Andreas Lochbihler:
fix LaTeX error
The file was modified src/HOL/Library/Bourbaki_Witt_Fixpoint.thy (diff)
Changeset 63561:fba08009ff3e by Andreas Lochbihler:
add lemmas contributed by Peter Gammie
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/BNF_Wellorder_Constructions.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
The file was modified src/HOL/Library/Bourbaki_Witt_Fixpoint.thy (diff)
The file was modified src/HOL/Library/Product_Order.thy (diff)
The file was modified src/HOL/Library/While_Combinator.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Order_Relation.thy (diff)
The file was modified src/HOL/Partial_Function.thy (diff)
The file was modified src/HOL/Relation.thy (diff)