src/FOL/FOL.thy
changeset 5887 0864c6578d16
parent 4854 d1850e0964f2
child 7355 4c43090659ca
equal deleted inserted replaced
5886:0373323180f5 5887:0864c6578d16
     2 FOL = IFOL +
     2 FOL = IFOL +
     3 
     3 
     4 rules
     4 rules
     5   classical "(~P ==> P) ==> P"
     5   classical "(~P ==> P) ==> P"
     6 
     6 
     7 setup
     7 setup ClasetThyData.setup
     8   ClasetThyData.setup
     8 setup attrib_setup              (* FIXME move to IFOL.thy *)
     9 
     9 
    10 end
    10 end