src/FOLP/IFOLP.thy
changeset 3942 1f1c1f524d19
parent 3836 f1a1817659e6
child 6509 9f7f4fd05b1f
equal deleted inserted replaced
3941:ea440c63d206 3942:1f1c1f524d19
     5 
     5 
     6 Intuitionistic First-Order Logic with Proofs
     6 Intuitionistic First-Order Logic with Proofs
     7 *)
     7 *)
     8 
     8 
     9 IFOLP = Pure +
     9 IFOLP = Pure +
       
    10 
       
    11 global
    10 
    12 
    11 classes term < logic
    13 classes term < logic
    12 
    14 
    13 default term
    15 default term
    14 
    16 
    56  exists         :: "['a,p]=>p"          ("(1[_,/_])")
    58  exists         :: "['a,p]=>p"          ("(1[_,/_])")
    57  xsplit         :: "[p,['a,p]=>p]=>p"
    59  xsplit         :: "[p,['a,p]=>p]=>p"
    58  ideq           :: "'a=>p"
    60  ideq           :: "'a=>p"
    59  idpeel         :: "[p,'a=>p]=>p"
    61  idpeel         :: "[p,'a=>p]=>p"
    60  nrm, NRM       :: "p"
    62  nrm, NRM       :: "p"
       
    63 
       
    64 local
    61 
    65 
    62 rules
    66 rules
    63 
    67 
    64 (**** Propositional logic ****)
    68 (**** Propositional logic ****)
    65 
    69