src/HOL/TPTP/TPTP_Parser_Test.thy
changeset 69366 b6dacf6eabe3
parent 68672 9247996782c9
equal deleted inserted replaced
69365:c5b3860d29ef 69366:b6dacf6eabe3
    45     @{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests
    45     @{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests
    46 end
    46 end
    47 
    47 
    48 (*test against all TPTP problems*)
    48 (*test against all TPTP problems*)
    49 fun problem_names () =
    49 fun problem_names () =
    50     map (Path.base_name #>
    50     map (Path.file_name #>
    51          TPTP_Problem_Name.parse_problem_name #>
    51          TPTP_Problem_Name.parse_problem_name #>
    52          TPTP_Problem_Name.mangle_problem_name)
    52          TPTP_Problem_Name.mangle_problem_name)
    53      (TPTP_Syntax.get_file_list tptp_probs_dir)
    53      (TPTP_Syntax.get_file_list tptp_probs_dir)
    54 \<close>
    54 \<close>
    55 
    55