Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. one last lemma about Total and Restr
  2. adjustments for fewer WO assumptions
  3. elimination of some needless assumptions
  4. merged
  5. iso lemmas
Changeset 72127:a0768f16bccd by paulson _lp15@cam.ac.uk_:
one last lemma about Total and Restr
The file was modified src/HOL/BNF_Wellorder_Constructions.thy (diff)
Changeset 72126:5de9a5fbf2ec by paulson _lp15@cam.ac.uk_:
adjustments for fewer WO assumptions
The file was modified src/HOL/Cardinals/Cardinal_Order_Relation.thy (diff)
The file was modified src/HOL/Cardinals/Ordinal_Arithmetic.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)
Changeset 72125:cf8399df4d76 by paulson _lp15@cam.ac.uk_:
elimination of some needless assumptions
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/BNF_Wellorder_Embedding.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
Changeset 72124:36220b07c047 by paulson:
merged
Changeset 72123:53b724b87eb3 by paulson _lp15@cam.ac.uk_:
iso lemmas
The file was modified src/HOL/BNF_Wellorder_Embedding.thy (diff)