src/FOLP/ROOT
author wenzelm
Mon, 26 Nov 2012 10:37:05 +0100
changeset 50210 747db833fbf7
parent 48738 f8c1a5b9488f
child 51397 03b586ee5930
permissions -rw-r--r--
no special treatment of control_reset, in accordance to other control styles;

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 FOLP

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