src/HOL/Tools/res_reconstruct.ML
changeset 25718 75d5d23a5c20
parent 25710 4cdf7de81e1b
child 25999 f8bcd311d501
equal deleted inserted replaced
25717:7f0647c6362f 25718:75d5d23a5c20
    93 (*Clause: a list of literals separated by the disjunction sign*)
    93 (*Clause: a list of literals separated by the disjunction sign*)
    94 val clause = $$"(" |-- literals --| $$")" || Scan.single literal;
    94 val clause = $$"(" |-- literals --| $$")" || Scan.single literal;
    95 
    95 
    96 val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
    96 val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
    97 
    97 
    98 (*<cnf_annotated> ::=Ęcnf(<name>,<formula_role>,<cnf_formula><annotations>).
    98 (*<cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula><annotations>).
    99   The <name> could be an identifier, but we assume integers.*)
    99   The <name> could be an identifier, but we assume integers.*)
   100 val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
   100 val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
   101                 integer --| $$"," -- Symbol.scan_id --| $$"," --
   101                 integer --| $$"," -- Symbol.scan_id --| $$"," --
   102                 clause -- Scan.option annotations --| $$ ")";
   102                 clause -- Scan.option annotations --| $$ ")";
   103 
   103