src/Pure/Syntax/mixfix.ML
changeset 12149 7cf8574102d5
parent 12121 55b71be171c5
child 12512 ab14b29dfc6d
equal deleted inserted replaced
12148:a57873aec3bf 12149:7cf8574102d5
    29   val const_name: string -> mixfix -> string
    29   val const_name: string -> mixfix -> string
    30   val fix_mixfix: string -> mixfix -> mixfix
    30   val fix_mixfix: string -> mixfix -> mixfix
    31   val mixfix_args: mixfix -> int
    31   val mixfix_args: mixfix -> int
    32   val pure_nonterms: string list
    32   val pure_nonterms: string list
    33   val pure_syntax: (string * string * mixfix) list
    33   val pure_syntax: (string * string * mixfix) list
       
    34   val pure_syntax_output: (string * string * mixfix) list
    34   val pure_appl_syntax: (string * string * mixfix) list
    35   val pure_appl_syntax: (string * string * mixfix) list
    35   val pure_applC_syntax: (string * string * mixfix) list
    36   val pure_applC_syntax: (string * string * mixfix) list
    36   val pure_xsym_syntax: (string * string * mixfix) list
    37   val pure_xsym_syntax: (string * string * mixfix) list
    37 end;
    38 end;
    38 
    39 
   238   ("_index",       "num_const => index",            Delimfix "\\<^sub>_"),
   239   ("_index",       "num_const => index",            Delimfix "\\<^sub>_"),
   239   ("_indexvar",    "index",                         Delimfix "\\<index>"),
   240   ("_indexvar",    "index",                         Delimfix "\\<index>"),
   240   ("_noindex",     "index",                         Delimfix ""),
   241   ("_noindex",     "index",                         Delimfix ""),
   241   ("_struct",      "index => logic",                Delimfix "\\<struct>_")];
   242   ("_struct",      "index => logic",                Delimfix "\\<struct>_")];
   242 
   243 
       
   244 val pure_syntax_output =
       
   245  [("Goal", "prop => prop", Mixfix ("_", [0], 0)),
       
   246   ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))];
       
   247 
   243 val pure_appl_syntax =
   248 val pure_appl_syntax =
   244  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),
   249  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),
   245   ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri))];
   250   ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri))];
   246 
   251 
   247 val pure_applC_syntax =
   252 val pure_applC_syntax =