Skip to content
This repository
Browse code

Bring across category theory in build-sequence and release notes for k7.

  • Loading branch information...
commit 2dc002e7e5bcc914e32a78832ae287091bb5171a 2 parents 97c64c8 + b5442c6
Michael Norrish authored

Showing 2 changed files with 4 additions and 0 deletions. Show diff stats Hide diff stats

  1. +2 0  doc/kananaskis-7.release.html
  2. +2 0  tools/build-sequence
2  doc/kananaskis-7.release.html
@@ -194,6 +194,8 @@ <h2 id="new-examples">New examples:</h2>
194 194 <ul>
195 195 <li> <p> A mechanisation of first-order and nominal unification done in an accumulator-passing style with <q>triangular</q> substitutions.
196 196 In <code>examples/unification/triangular</code>.
  197 +<li><p> Some basic category theory (up to the Yoneda lemma), including two categories of <q>sets</q>: one using HOL sets (predicates) and one using the axiomatically introduced type from <code>zfsetTheory</code>.
  198 +In <code>examples/category</code>.
197 199 </ul>
198 200
199 201 <h2 id="incompatibilities">Incompatibilities:</h2>
2  tools/build-sequence
@@ -151,6 +151,8 @@ src/temporal/src
151 151 # Examples only from here on
152 152 #
153 153 !examples/MLsyntax
  154 +!examples/zfset
  155 +!!examples/category
154 156 !!examples/miller/ho_prover
155 157 !!examples/miller/miller
156 158 !examples/ordinal

0 comments on commit 2dc002e

Please sign in to comment.
Something went wrong with that request. Please try again.