src/FOLP/ROOT.ML
changeset 25750 4e796867ccb5
parent 17480 fd19f77dcf60
child 33615 261abc2e3155
equal deleted inserted replaced
25749:10e7feb4e595 25750:4e796867ccb5
     6 Modifed version of Lawrence Paulson's FOL that contains proof terms.
     6 Modifed version of Lawrence Paulson's FOL that contains proof terms.
     7 
     7 
     8 Presence of unknown proof term means that matching does not behave as expected.
     8 Presence of unknown proof term means that matching does not behave as expected.
     9 *)
     9 *)
    10 
    10 
    11 val banner = "First-Order Logic with Natural Deduction with Proof Terms";
    11 use_thy "FOLP";
    12 writeln banner;
       
    13 
    12 
    14 use_thy "FOLP";