src/FOLP/ROOT
author haftmann
Thu Nov 23 17:03:27 2017 +0000 (20 months ago)
changeset 67087 733017b19de9
parent 66946 3d8fd98c7c86
child 69272 15e9ed5b28fb
permissions -rw-r--r--
generalized more lemmas
     1 chapter FOLP
     2 
     3 session FOLP = Pure +
     4   description {*
     5     Author:     Martin Coen, Cambridge University Computer Laboratory
     6     Copyright   1993  University of Cambridge
     7 
     8     Modifed version of FOL that contains proof terms.
     9 
    10     Presence of unknown proof term means that matching does not behave as expected.
    11   *}
    12   theories
    13     IFOLP (global)
    14     FOLP (global)
    15 
    16 session "FOLP-ex" in ex = FOLP +
    17   description {*
    18     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19     Copyright   1992  University of Cambridge
    20 
    21     Examples for First-Order Logic.
    22   *}
    23   theories
    24     Intro
    25     Nat
    26     Foundation
    27     If
    28     Intuitionistic
    29     Classical
    30     Propositional_Int
    31     Quantifiers_Int
    32     Propositional_Cla
    33     Quantifiers_Cla