From 4ac94138305ffa889f3ffea8d478f44ab610cee8 Mon Sep 17 00:00:00 2001 From: jesse-michael-han Date: Tue, 22 Oct 2019 01:13:45 -0400 Subject: [PATCH] Prepare for release Fix error Add links --- README.org | 2 ++ src/summary.lean | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/README.org b/README.org index 1346a16..4fdd967 100644 --- a/README.org +++ b/README.org @@ -66,6 +66,8 @@ A summary of the main results can be found in [[src/summary.lean]], containing ~ We also have a formula pretty-printer which prints de Bruijn indexed-formulas as their named representations. Code and examples for the pretty-printer can be found in [[src/print_formula.lean]]. *** Papers +Our paper /A formal proof of the independence of the continuum hypothesis/, describing [[https://github.com/flypitch/flypitch/releases/tag/2.1][this release]], has been submitted to [[https://popl20.sigplan.org/home/CPP-2020][CPP 2020]]. It is available [[https://github.com/flypitch/flypitch-cpp-2020/releases/tag/1.0][here]]. + Our paper /A formalization of forcing and the unprovability of the continuum hypothesis/, describing [[https://github.com/flypitch/flypitch/releases/tag/1.2][this release]], was accepted to [[https://itp19.cecs.pdx.edu/][ITP 2019]]. It is available [[https://github.com/flypitch/flypitch-itp-2019/releases/tag/1.1][here]]. **** Citation information: diff --git a/src/summary.lean b/src/summary.lean index 9779f26..1499b9f 100644 --- a/src/summary.lean +++ b/src/summary.lean @@ -46,7 +46,7 @@ This file summarizes: #print ZFC -#eval print_formula_list ([axiom_of_emptyset, axiom_of_pairing, axiom_of_extensionality, axiom_of_union, axiom_of_powerset, axiom_of_infinity, axiom_of_regularity, zorns_lemma]) +#eval print_formula_list ([axiom_of_emptyset, axiom_of_ordered_pairs, axiom_of_extensionality, axiom_of_union, axiom_of_powerset, axiom_of_infinity, axiom_of_regularity, zorns_lemma]) #print CH