src/FOLP/ROOT
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 51397 03b586ee5930
child 65527 0d8a7013bf36
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     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   options [document = false]
    13   theories FOLP
    14 
    15 session "FOLP-ex" in ex = FOLP +
    16   description {*
    17     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18     Copyright   1992  University of Cambridge
    19 
    20     Examples for First-Order Logic.
    21   *}
    22   options [document = false]
    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
    34