src/HOL/TPTP/TPTP_Parser_Example.thy
changeset 47790 2e1636e45770
parent 47687 bfbd2d0bb348
child 48891 c0eafbd55de3
equal deleted inserted replaced
47789:71a526ee569a 47790:2e1636e45770
     4 Example of importing a TPTP problem and trying to prove it in Isabelle/HOL.
     4 Example of importing a TPTP problem and trying to prove it in Isabelle/HOL.
     5 *)
     5 *)
     6 
     6 
     7 theory TPTP_Parser_Example
     7 theory TPTP_Parser_Example
     8 imports TPTP_Parser TPTP_Interpret
     8 imports TPTP_Parser TPTP_Interpret
     9 uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
     9 uses "sledgehammer_tactics.ML"
    10 begin
    10 begin
    11 
    11 
    12 import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
    12 import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
    13 
    13 
    14 ML {*
    14 ML {*