Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Missing theorem restored
  2. Tidying up BNF
  3. More cleaning up proofs, plus a TeX fix
Changeset 76952:f552cf789a8d by paulson _lp15@cam.ac.uk_:
Missing theorem restored
The file was modified src/HOL/BNF_Cardinal_Arithmetic.thy (diff)
Changeset 76951:293caf3dbecd by paulson _lp15@cam.ac.uk_:
Tidying up BNF
The file was modified src/HOL/BNF_Cardinal_Arithmetic.thy (diff)
The file was modified src/HOL/BNF_Cardinal_Order_Relation.thy (diff)
The file was modified src/HOL/Cardinals/Cardinal_Order_Relation.thy (diff)
Changeset 76950:f881fd264929 by paulson _lp15@cam.ac.uk_:
More cleaning up proofs, plus a TeX fix
The file was modified src/HOL/BNF_Wellorder_Constructions.thy (diff)
The file was modified src/HOL/BNF_Wellorder_Embedding.thy (diff)
The file was modified src/HOL/BNF_Wellorder_Relation.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)