Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. tuned;
  3. tuned proofs;
  4. Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
  5. clarified lfp/gfp statements and proofs;
Changeset 63983:db9259a5e20e by wenzelm:
merged
Changeset 63982:4c4049e3bad8 by wenzelm:
tuned;
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 63981:6f7db4f8df4c by wenzelm:
tuned proofs;
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
Changeset 63980:f8e556c8ad6f by wenzelm:
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
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 removedsrc/HOL/Isar_Examples/Schroeder_Bernstein.thy
Changeset 63979:95c3ae4baba8 by wenzelm:
clarified lfp/gfp statements and proofs;
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)