src/FOLP/ROOT
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57009 8cb6a5f1ae84
parent 51397 03b586ee5930
child 65527 0d8a7013bf36
permissions -rw-r--r--
added SML implementation of MaSh
wenzelm@51397
     1
chapter FOLP
wenzelm@51397
     2
wenzelm@48738
     3
session FOLP = Pure +
wenzelm@48475
     4
  description {*
wenzelm@48475
     5
    Author:     Martin Coen, Cambridge University Computer Laboratory
wenzelm@48475
     6
    Copyright   1993  University of Cambridge
wenzelm@48475
     7
wenzelm@48475
     8
    Modifed version of FOL that contains proof terms.
wenzelm@48475
     9
wenzelm@48475
    10
    Presence of unknown proof term means that matching does not behave as expected.
wenzelm@48475
    11
  *}
wenzelm@48483
    12
  options [document = false]
wenzelm@48475
    13
  theories FOLP
wenzelm@48475
    14
wenzelm@48738
    15
session "FOLP-ex" in ex = FOLP +
wenzelm@48475
    16
  description {*
wenzelm@48475
    17
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48475
    18
    Copyright   1992  University of Cambridge
wenzelm@48475
    19
wenzelm@48475
    20
    Examples for First-Order Logic.
wenzelm@48475
    21
  *}
wenzelm@48483
    22
  options [document = false]
wenzelm@48475
    23
  theories
wenzelm@48475
    24
    Intro
wenzelm@48475
    25
    Nat
wenzelm@48475
    26
    Foundation
wenzelm@48475
    27
    If
wenzelm@48475
    28
    Intuitionistic
wenzelm@48475
    29
    Classical
wenzelm@48475
    30
    Propositional_Int
wenzelm@48475
    31
    Quantifiers_Int
wenzelm@48475
    32
    Propositional_Cla
wenzelm@48475
    33
    Quantifiers_Cla
wenzelm@48475
    34