Summary
- merged
- tuned;
- tuned proofs;
- Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
- clarified lfp/gfp statements and proofs;
The file was modified | src/HOL/Finite_Set.thy (diff) |
The file was modified | src/HOL/Wellfounded.thy (diff) |
The file was modified | src/HOL/Hilbert_Choice.thy (diff) |
The file was modified | src/HOL/Inductive.thy (diff) |
The file was modified | src/HOL/BNF_Cardinal_Order_Relation.thy (diff) |
The file was modified | src/HOL/Hilbert_Choice.thy (diff) |
The file was modified | src/HOL/Inductive.thy (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was removed | src/HOL/Isar_Examples/Schroeder_Bernstein.thy |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Complete_Partial_Order.thy (diff) |
The file was modified | src/HOL/Inductive.thy (diff) |
The file was modified | src/HOL/Library/Extended_Nonnegative_Real.thy (diff) |
The file was modified | src/HOL/Library/Order_Continuity.thy (diff) |
The file was modified | src/HOL/Nat.thy (diff) |