Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOLP/ROOT
author wenzelm
Sun, 21 May 2017 23:41:46 +0200
changeset 65895 744878d72021
parent 65527 0d8a7013bf36
child 66946 3d8fd98c7c86
permissions -rw-r--r--
more general workaround for failed sessions (again, see also 2edb89630a80, ed7b5cd3a7f2);

chapter FOLP

session FOLP = Pure +
  description {*
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

    Modifed version of FOL that contains proof terms.

    Presence of unknown proof term means that matching does not behave as expected.
  *}
  options [document = false]
  theories
    IFOLP (global)
    FOLP (global)

session "FOLP-ex" in ex = FOLP +
  description {*
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

    Examples for First-Order Logic.
  *}
  options [document = false]
  theories
    Intro
    Nat
    Foundation
    If
    Intuitionistic
    Classical
    Propositional_Int
    Quantifiers_Int
    Propositional_Cla
    Quantifiers_Cla
isabelle