src/LCF/LCF.thy
changeset 17249 e89fbfd778c1
parent 17248 81bf91654e73
child 19757 4a2a71c31968
equal deleted inserted replaced
17248:81bf91654e73 17249:e89fbfd778c1
     6 
     6 
     7 header {* LCF on top of First-Order Logic *}
     7 header {* LCF on top of First-Order Logic *}
     8 
     8 
     9 theory LCF
     9 theory LCF
    10 imports FOL
    10 imports FOL
    11 uses ("pair.ML") ("fix.ML")
    11 uses ("LCF_lemmas.ML") ("pair.ML") ("fix.ML")
    12 begin
    12 begin
    13 
    13 
    14 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
    14 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
    15 
    15 
    16 subsection {* Natural Deduction Rules for LCF *}
    16 subsection {* Natural Deduction Rules for LCF *}