src/FOLP/FOLP.thy
author wenzelm
Fri Oct 10 16:29:41 1997 +0200 (1997-10-10)
changeset 3836 f1a1817659e6
parent 1477 4c51ab632cda
child 17480 fd19f77dcf60
permissions -rw-r--r--
fixed dots;
     1 (*  Title:      FOLP/FOLP.thy
     2     ID:         $Id$
     3     Author:     Martin D Coen, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Classical First-Order Logic with Proofs
     7 *)
     8 
     9 FOLP = IFOLP +
    10 consts
    11   cla :: "[p=>p]=>p"
    12 rules
    13   classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    14 end