src/Pure/pure_thy.ML
changeset 42296 dcc08f2a8671
parent 42295 8fdbb3b10beb
child 42297 140f283266b7
equal deleted inserted replaced
42295:8fdbb3b10beb 42296:dcc08f2a8671
   135     ("_update_name", typ "idt",                        NoSyn),
   135     ("_update_name", typ "idt",                        NoSyn),
   136     ("_constrainAbs", typ "'a",                        NoSyn),
   136     ("_constrainAbs", typ "'a",                        NoSyn),
   137     ("_constrain_position", typ "id => id_position",   Delimfix "_"),
   137     ("_constrain_position", typ "id => id_position",   Delimfix "_"),
   138     ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
   138     ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
   139     ("_type_constraint_", typ "'a",                    NoSyn),
   139     ("_type_constraint_", typ "'a",                    NoSyn),
   140     ("_context_const", typ "id => logic",              Delimfix "CONST _"),
   140     ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
   141     ("_context_const", typ "id => aprop",              Delimfix "CONST _"),
   141     ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
   142     ("_context_const", typ "longid => logic",          Delimfix "CONST _"),
   142     ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
   143     ("_context_const", typ "longid => aprop",          Delimfix "CONST _"),
   143     ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
   144     ("_context_xconst", typ "id => logic",             Delimfix "XCONST _"),
   144     ("_context_xconst", typ "id_position => logic",    Delimfix "XCONST _"),
   145     ("_context_xconst", typ "id => aprop",             Delimfix "XCONST _"),
   145     ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
   146     ("_context_xconst", typ "longid => logic",         Delimfix "XCONST _"),
   146     ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
   147     ("_context_xconst", typ "longid => aprop",         Delimfix "XCONST _"),
   147     ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
   148     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
   148     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
   149     (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
   149     (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
   150     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   150     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   151     (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
   151     (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
   152     (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
   152     (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]