equal
deleted
inserted
replaced
54 |
54 |
55 val dummy_satallax_step = ((("~1", "tab_inh"), AAtom (ATerm(("False", []), []))), NONE) |
55 val dummy_satallax_step = ((("~1", "tab_inh"), AAtom (ATerm(("False", []), []))), NONE) |
56 fun parse_tstp_thf0_satallax_line x = |
56 fun parse_tstp_thf0_satallax_line x = |
57 (((Scan.this_string tptp_thf |
57 (((Scan.this_string tptp_thf |
58 -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," |
58 -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," |
59 -- parse_thf_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") |
59 -- parse_hol_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") |
60 || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") |
60 || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") |
61 >> K dummy_satallax_step) x |
61 >> K dummy_satallax_step) x |
62 |
62 |
63 datatype satallax_step = Satallax_Step of { |
63 datatype satallax_step = Satallax_Step of { |
64 id: string, |
64 id: string, |