Summary
- merged
- prefer [simp] over [iff] as [iff] break HOL-UNITY
- fix LaTeX error
- add lemmas contributed by Peter Gammie
The file was modified | src/HOL/Order_Relation.thy (diff) |
The file was modified | src/HOL/Relation.thy (diff) |
The file was modified | src/HOL/Library/Bourbaki_Witt_Fixpoint.thy (diff) |
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) |