src/Pure/Syntax/type_ext.ML
changeset 9067 64464b5f6867
parent 8895 2913a54e64cf
child 10572 b070825579b8
equal deleted inserted replaced
9066:b1e874e38dab 9067:64464b5f6867
   173    Mfix ("_",           longidT --> classesT,          "", [], max_pri),
   173    Mfix ("_",           longidT --> classesT,          "", [], max_pri),
   174    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   174    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   175    Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
   175    Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
   176    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   176    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   177    Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
   177    Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
   178    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   178    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   179    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
   179    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> 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),