Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. Completeness proof for open formulas. Proofs in declarative style. Enumerations using Countable theory. (Contributed by Andreas Halkjær From with cosmetic changes by Stefan Berghofer)
  2. Proof of Andrew’s Challenge, a bit of tidying and updated metadata.
  3. corrected reference to metadata file
Changeset 9615:987bfc80e3ac by anders schlichtkrull _andschl@dtu.dk_:
Completeness proof for open formulas. Proofs in declarative style. Enumerations using Countable theory. (Contributed by Andreas Halkjær From with cosmetic changes by Stefan Berghofer)
The file was modified metadata/metadata
The file was modified thys/FOL-Fitting/FOL_Fitting.thy
Changeset 9614:d7a4f0f8a290 by anders schlichtkrull _andschl@dtu.dk_:
Proof of Andrew’s Challenge, a bit of tidying and updated metadata.
The file was modified metadata/metadata
The file was modified thys/FOL_Harrison/FOL_Harrison.thy
Changeset 9613:3f604a2c8858 by anders schlichtkrull _andschl@dtu.dk_:
corrected reference to metadata file
The file was modified doc/maintenance.md