src/FOL/FOL.thy
author paulson
Sat, 10 Jan 1998 17:59:32 +0100
changeset 4552 bb8ff763c93d
parent 4093 5e8f3d57dee7
child 4793 03fd006fb97b
permissions -rw-r--r--
Simplified proofs by omitting PA = {|XA, ...|} from RA2


FOL = IFOL +

rules
  classical "(~P ==> P) ==> P"

end

ML val thy_data = [ClasetThyData.thy_data];