src/Pure/Syntax/type_ext.ML
changeset 2678 d5fe793293ac
parent 2584 b386951e15e6
child 2699 932fae4271d7
equal deleted inserted replaced
2677:d73a46247a4a 2678:d5fe793293ac
   179    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   179    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   180    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   180    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   181    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   181    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   182    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   182    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   183    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   183    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   184    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri)]
   184    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
       
   185    Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
   185   []
   186   []
   186   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
   187   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
   187    [],
   188    [],
   188    [],
   189    [],
   189    [("fun", fun_ast_tr')])
   190    [("fun", fun_ast_tr')])