Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Fixed a broken proof
  2. Substantial simplification of HOL-Cardinals
  3. merged
  4. Trying to clean up HOL/Cardinals
Changeset 76949:ec4c38e156c7 by paulson _lp15@cam.ac.uk_:
Fixed a broken proof
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)
Changeset 76948:f33df7529fed by paulson _lp15@cam.ac.uk_:
Substantial simplification of HOL-Cardinals
The file was modified src/HOL/Cardinals/Order_Union.thy (diff)
The file was modified src/HOL/Cardinals/Ordinal_Arithmetic.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Embedding.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Relation.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76947:20ab27bc1f3b by paulson:
merged
Changeset 76946:5df58a471d9e by paulson _lp15@cam.ac.uk_:
Trying to clean up HOL/Cardinals
The file was modified src/HOL/Cardinals/Cardinal_Arithmetic.thy (diff)
The file was modified src/HOL/Cardinals/Cardinal_Order_Relation.thy (diff)
The file was modified src/HOL/Cardinals/Fun_More.thy (diff)
The file was modified src/HOL/Cardinals/Order_Relation_More.thy (diff)
The file was modified src/HOL/Cardinals/Order_Union.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)