src/Pure/Syntax/type_ext.ML
changeset 624 33b9b5da3e6f
parent 557 9d386e6c02b7
child 640 b26753b92f98
equal deleted inserted replaced
623:ca9f5dbab880 624:33b9b5da3e6f
   175    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   175    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   176    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   176    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   177    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   177    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   178    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   178    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   179    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   179    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   180    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)]
   180    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
       
   181    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri)]
   181   []
   182   []
   182   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
   183   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
   183    [],
   184    [],
   184    [],
   185    [],
   185    [("fun", fun_ast_tr')])
   186    [("fun", fun_ast_tr')])