Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Tidying of some very old proofs
  2. merged
  3. tidying of some old proofs
  4. merged
  5. new contributor
  6. more List lemmas (partly by Jeremy Sylvestre)
  7. merged
  8. merged
  9. Trying to clean up some messy proofs
  10. Mostly, removing the unfold method
  11. Mostly trivial simplifications
  12. Removal of the "unfold" method in favour of "unfolding"
  13. Elimination of the archaic ASCII syntax
  14. strengthened lemmas preorder.reflp_ge[simp] and preorder.reflp_le[simp]
  15. added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]
Changeset 76299:0ad6f6508274 by paulson _lp15@cam.ac.uk_:
Tidying of some very old proofs
The file was modified src/HOL/Auth/Event.thy (diff)
The file was modified src/HOL/Auth/KerberosIV.thy (diff)
The file was modified src/HOL/Auth/KerberosV.thy (diff)
The file was modified src/HOL/Auth/Kerberos_BAN.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Auth/NS_Public.thy (diff)
The file was modified src/HOL/Auth/NS_Public_Bad.thy (diff)
The file was modified src/HOL/Auth/NS_Shared.thy (diff)
The file was modified src/HOL/Auth/OtwayRees.thy (diff)
The file was modified src/HOL/Auth/Smartcard/Smartcard.thy (diff)
Changeset 76298:efc220128637 by paulson:
merged
Changeset 76297:e7f9e5b3a36a by paulson _lp15@cam.ac.uk_:
tidying of some old proofs
The file was modified src/HOL/Auth/NS_Public.thy (diff)
The file was modified src/HOL/Auth/NS_Public_Bad.thy (diff)
The file was modified src/HOL/Auth/OtwayRees.thy (diff)
Changeset 76296:eb30869e7228 by nipkow:
merged
Changeset 76295:77e13a694cbe by nipkow:
new contributor
The file was modified CONTRIBUTORS (diff)
Changeset 76294:642f1a36e1d6 by nipkow:
more List lemmas (partly by Jeremy Sylvestre)
The file was modified src/HOL/List.thy (diff)
Changeset 76293:f3e30ad850ba by paulson:
merged
Changeset 76292:2317e9a19239 by paulson:
merged
Changeset 76291:616405057951 by paulson _lp15@cam.ac.uk_:
Trying to clean up some messy proofs
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Auth/NS_Public_Bad.thy (diff)
Changeset 76290:64d29ebb7d3d by paulson _lp15@cam.ac.uk_:
Mostly, removing the unfold method
The file was modified src/HOL/Auth/Guard/Proto.thy (diff)
The file was modified src/HOL/Auth/KerberosIV.thy (diff)
The file was modified src/HOL/Auth/KerberosIV_Gets.thy (diff)
The file was modified src/HOL/Auth/KerberosV.thy (diff)
The file was modified src/HOL/Auth/Kerberos_BAN.thy (diff)
The file was modified src/HOL/Auth/Kerberos_BAN_Gets.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Auth/Public.thy (diff)
The file was modified src/HOL/Auth/Recur.thy (diff)
The file was modified src/HOL/Auth/Shared.thy (diff)
The file was modified src/HOL/Auth/Smartcard/Smartcard.thy (diff)
Changeset 76289:a6cc15ec45b2 by paulson _lp15@cam.ac.uk_:
Mostly trivial simplifications
The file was modified src/HOL/Auth/Guard/Extensions.thy (diff)
The file was modified src/HOL/Auth/Guard/Proto.thy (diff)
The file was modified src/HOL/Auth/KerberosIV.thy (diff)
The file was modified src/HOL/Auth/KerberosIV_Gets.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Auth/OtwayReesBella.thy (diff)
The file was modified src/HOL/Auth/Public.thy (diff)
The file was modified src/HOL/Auth/Yahalom.thy (diff)
Changeset 76288:b82ac7ef65ec by paulson _lp15@cam.ac.uk_:
Removal of the "unfold" method in favour of "unfolding"
The file was modified src/HOL/Auth/Guard/Extensions.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_NS_Public.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_OtwayRees.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_Yahalom.thy (diff)
The file was modified src/HOL/Auth/Guard/P1.thy (diff)
The file was modified src/HOL/Auth/Guard/P2.thy (diff)
The file was modified src/HOL/Auth/Guard/Proto.thy (diff)
The file was modified src/HOL/Auth/KerberosIV.thy (diff)
The file was modified src/HOL/Auth/KerberosIV_Gets.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Auth/Public.thy (diff)
The file was modified src/HOL/Auth/Yahalom.thy (diff)
Changeset 76287:cdc14f94c754 by paulson _lp15@cam.ac.uk_:
Elimination of the archaic ASCII syntax
The file was modified src/HOL/Auth/CertifiedEmail.thy (diff)
The file was modified src/HOL/Auth/Event.thy (diff)
The file was modified src/HOL/Auth/Guard/Analz.thy (diff)
The file was modified src/HOL/Auth/Guard/Extensions.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard.thy (diff)
The file was modified src/HOL/Auth/Guard/GuardK.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_NS_Public.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_OtwayRees.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_Public.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_Shared.thy (diff)
The file was modified src/HOL/Auth/Guard/Guard_Yahalom.thy (diff)
The file was modified src/HOL/Auth/Guard/List_Msg.thy (diff)
The file was modified src/HOL/Auth/Guard/P1.thy (diff)
The file was modified src/HOL/Auth/Guard/P2.thy (diff)
The file was modified src/HOL/Auth/Guard/Proto.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Auth/NS_Shared.thy (diff)
The file was modified src/HOL/Auth/OtwayReesBella.thy (diff)
The file was modified src/HOL/Auth/OtwayRees_AN.thy (diff)
The file was modified src/HOL/Auth/OtwayRees_Bad.thy (diff)
The file was modified src/HOL/Auth/Public.thy (diff)
The file was modified src/HOL/Auth/Recur.thy (diff)
The file was modified src/HOL/Auth/Shared.thy (diff)
The file was modified src/HOL/Auth/TLS.thy (diff)
The file was modified src/HOL/Auth/WooLam.thy (diff)
The file was modified src/HOL/Auth/Yahalom_Bad.thy (diff)
The file was modified src/HOL/Auth/ZhouGollmann.thy (diff)
Changeset 76286:a00c80314b06 by desharna:
strengthened lemmas preorder.reflp_ge[simp] and preorder.reflp_le[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76285:8e777e0e206a by desharna:
added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)