src/HOL/Tools/ATP/atp_proof.ML
changeset 51880 46d911ab9170
parent 51367 4b5a5e26161d
child 51881 475c2eab2d7c
equal deleted inserted replaced
51879:ee9562d31778 51880:46d911ab9170
   213 (**** PARSING OF TSTP FORMAT ****)
   213 (**** PARSING OF TSTP FORMAT ****)
   214 
   214 
   215 (* Strings enclosed in single quotes (e.g., file names) *)
   215 (* Strings enclosed in single quotes (e.g., file names) *)
   216 val scan_general_id =
   216 val scan_general_id =
   217   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   217   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   218   || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
   218   || Scan.repeat ($$ "$") -- Scan.many1 (fn s => Symbol.is_letdig s orelse s="-")
   219      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
   219      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
   220 
   220 
   221 val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode
   221 val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode
   222 
   222 
   223 val skip_term =
   223 val skip_term =