Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. added Mirabelle action presburger
  2. added timing to Mirabelle action arith
  3. added error message on invalid Mirabelle action
Changeset 74516:2c093a3167d1 by desharna:
added Mirabelle action presburger
The file was addedsrc/HOL/Tools/Mirabelle/mirabelle_presburger.ML
The file was modified src/HOL/Mirabelle.thy
Changeset 74515:64c0d78d2f19 by desharna:
added timing to Mirabelle action arith
The file was modified src/HOL/Tools/Mirabelle/mirabelle_arith.ML
Changeset 74514:9a2d290a3a0b by desharna:
added error message on invalid Mirabelle action
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML

Summary

  1. CZH: large limits, generalizations, a variety of minor amendments
Changeset 12092:aedbb5773de3 by user9716869 _user9716869@gmail.com_:
CZH: large limits, generalizations, a variety of minor amendments
The file was modified thys/CZH_Elementary_Categories/ROOT
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Discrete.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_FUNCT.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Functor.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Set.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Category.thy
The file was modified thys/CZH_Foundations/ROOT
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_GRPH.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Introduction.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_Semicategory.thy
The file was modified thys/CZH_Foundations/document/root.bib
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Complete.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Kan.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan_Example.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Universal.thy