History log of /seL4-l4v-master/HOL4/examples/logic/folcompactness/folPrenexScript.sml
Revision Date Author Comments
# 46d42c2d 23-Mar-2020 Michael Norrish <michael.norrish@data61.csiro.au>

Fix proof broken by 508f79ea974
# c93afcec 04-Aug-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Complete port of HOL Light material on skolemization

A couple more files to go.
# 922e2366 29-Jul-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Progress with port of HOL Light compactness etc theories
# 97dbc36b 29-Jul-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Start port of material about f.o. compactness from HOL Light

See commit

https://github.com/jrh13/hol-light/commit/013324af7ff715346383fb963d323138cf011732

Thanks to John for making this available (some of it is behind his
TPHOLs 1998 paper.)