src/Tools/isac/BaseDefinitions/parseC.sml
changeset 60661 91c30b11e5bc
parent 60660 c4b24621077e
child 60697 dd386fd3ec5e
equal deleted inserted replaced
60660:c4b24621077e 60661:91c30b11e5bc
     2    Author: Walther Neuper
     2    Author: Walther Neuper
     3    (c) due to copyright terms
     3    (c) due to copyright terms
     4 *)
     4 *)
     5 signature PARSE_ISAC =
     5 signature PARSE_ISAC =
     6 sig
     6 sig
       
     7   val term_position: Proof.context -> string * Position.T -> term
     7   val pattern_position: Proof.context -> string * Position.T -> term
     8   val pattern_position: Proof.context -> string * Position.T -> term
     8   val term_position: Proof.context -> string * Position.T -> term
       
     9 
     9 
    10   val term_opt: Proof.context -> string -> term option
    10   val term_opt: Proof.context -> string -> term option
    11   val patt_opt: theory -> string -> term option
    11   val patt_opt: theory -> string -> term option
    12 
    12 
    13   val parse_test: Proof.context -> string -> term
    13   val parse_test: Proof.context -> string -> term