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