src/HOL/TPTP/TPTP_Parser_Example.thy
changeset 47687 bfbd2d0bb348
parent 47558 55b42f9af99d
child 47790 2e1636e45770
     1.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Mon Apr 23 12:23:23 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Mon Apr 23 12:23:23 2012 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
     1.5  begin
     1.6  
     1.7 -import_tptp "$TPTP/Problems/ALG/ALG001^5.p"
     1.8 +import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
     1.9  
    1.10  ML {*
    1.11  val an_fmlas =